kernel/linux.git/tools/memory-model/linux-kernel.cat, branch v6.19.11

tools/memory-model: Define effect of Mb tags on RMWs in tools/...

2025-02-20T15:40:23+00:00

Herd7 transforms successful RMW with Mb tags by inserting smp_mb() fences around them. We emulate this by considering imaginary po-edges before the RMW read and before the RMW write, and extending the smp_mb() ordering rule, which currently only applies to real po edges that would be found around a really inserted smp_mb(), also to cases of the only imagined po edges. Reported-by: Viktor Vafeiadis Suggested-by: Alan Stern Signed-off-by: Jonas Oberhauser Signed-off-by: Paul E. McKenney Reviewed-by: Boqun Feng Tested-by: Boqun Feng

tools/memory-model: Make ppo a subrelation of po

2023-03-22T19:02:21+00:00

As stated in the documentation and implied by its name, the ppo (preserved program order) relation is intended to link po-earlier to po-later instructions under certain conditions. However, a corner case currently allows instructions to be linked by ppo that are not executed by the same thread, i.e., instructions are being linked that have no po relation. This happens due to the mb/strong-fence/fence relations, which (as one case) provide order when locks are passed between threads followed by an smp_mb__after_unlock_lock() fence. This is illustrated in the following litmus test (as can be seen when using herd7 with `doshow ppo`): P0(spinlock_t *x, spinlock_t *y) { spin_lock(x); spin_unlock(x); } P1(spinlock_t *x, spinlock_t *y) { spin_lock(x); smp_mb__after_unlock_lock(); *y = 1; } The ppo relation will link P0's spin_lock(x) and P1's *y=1, because P0 passes a lock to P1 which then uses this fence. The patch makes ppo a subrelation of po by letting fence contribute to ppo only in case the fence links events of the same thread. Signed-off-by: Jonas Oberhauser Acked-by: Alan Stern Acked-by: Andrea Parri Signed-off-by: Paul E. McKenney

tools/memory-model: Restrict to-r to read-read address dependency

2023-03-22T19:02:21+00:00

During a code-reading exercise of linux-kernel.cat CAT file, I generated a graph to show the to-r relations. While likely not problematic for the model, I found it confusing that a read-write address dependency would show as a to-r edge on the graph. This patch therefore restricts the to-r links derived from addr to only read-read address dependencies, so that read-write address dependencies don't show as to-r in the graphs. This should also prevent future users of to-r from deriving incorrect relations. Note that a read-write address dep, obviously, still ends up in the ppo relation via the to-w relation. I verified that a read-read address dependency still shows up as a to-r link in the graph, as it did before. For reference, the problematic graph was generated with the following command: herd7 -conf linux-kernel.cfg \ -doshow dep -doshow to-r -doshow to-w ./foo.litmus -show all -o OUT/ Signed-off-by: Joel Fernandes (Google) Acked-by: Alan Stern Acked-by: Andrea Parri Signed-off-by: Paul E. McKenney

tools/memory-model: Add smp_mb__after_srcu_read_unlock()

2023-03-22T19:02:21+00:00

This commit adds support for smp_mb__after_srcu_read_unlock(), which, when combined with a prior srcu_read_unlock(), implies a full memory barrier. No ordering is guaranteed to accesses between the two, and placing accesses between is bad practice in any case. Tests may be found at https://github.com/paulmckrcu/litmus in files matching manual/kernel/C-srcu-mb-*.litmus. Signed-off-by: Paul E. McKenney

tools/memory-model: Unify UNLOCK+LOCK pairings to po-unlock-lock-po

2023-03-22T19:02:21+00:00

LKMM uses two relations for talking about UNLOCK+LOCK pairings: 1) po-unlock-lock-po, which handles UNLOCK+LOCK pairings on the same CPU or immediate lock handovers on the same lock variable 2) po;[UL];(co|po);[LKW];po, which handles UNLOCK+LOCK pairs literally as described in rcupdate.h#L1002, i.e., even after a sequence of handovers on the same lock variable. The latter relation is used only once, to provide the guarantee defined in rcupdate.h#L1002 by smp_mb__after_unlock_lock(), which makes any UNLOCK+LOCK pair followed by the fence behave like a full barrier. This patch drops this use in favor of using po-unlock-lock-po everywhere, which unifies the way the model talks about UNLOCK+LOCK pairings. At first glance this seems to weaken the guarantee given by LKMM: When considering a long sequence of lock handovers such as below, where P0 hands the lock to P1, which hands it to P2, which finally executes such an after_unlock_lock fence, the mb relation currently links any stores in the critical section of P0 to instructions P2 executes after its fence, but not so after the patch. P0(int *x, int *y, spinlock_t *mylock) { spin_lock(mylock); WRITE_ONCE(*x, 2); spin_unlock(mylock); WRITE_ONCE(*y, 1); } P1(int *y, int *z, spinlock_t *mylock) { int r0 = READ_ONCE(*y); // reads 1 spin_lock(mylock); spin_unlock(mylock); WRITE_ONCE(*z,1); } P2(int *z, int *d, spinlock_t *mylock) { int r1 = READ_ONCE(*z); // reads 1 spin_lock(mylock); spin_unlock(mylock); smp_mb__after_unlock_lock(); WRITE_ONCE(*d,1); } P3(int *x, int *d) { WRITE_ONCE(*d,2); smp_mb(); WRITE_ONCE(*x,1); } exists (1:r0=1 /\ 2:r1=1 /\ x=2 /\ d=2) Nevertheless, the ordering guarantee given in rcupdate.h is actually not weakened. This is because the unlock operations along the sequence of handovers are A-cumulative fences. They ensure that any stores that propagate to the CPU performing the first unlock operation in the sequence must also propagate to every CPU that performs a subsequent lock operation in the sequence. Therefore any such stores will also be ordered correctly by the fence even if only the final handover is considered a full barrier. Indeed this patch does not affect the behaviors allowed by LKMM at all. The mb relation is used to define ordering through: 1) mb/.../ppo/hb, where the ordering is subsumed by hb+ where the lock-release, rfe, and unlock-acquire orderings each provide hb 2) mb/strong-fence/cumul-fence/prop, where the rfe and A-cumulative lock-release orderings simply add more fine-grained cumul-fence edges to substitute a single strong-fence edge provided by a long lock handover sequence 3) mb/strong-fence/pb and various similar uses in the definition of data races, where as discussed above any long handover sequence can be turned into a sequence of cumul-fence edges that provide the same ordering. Signed-off-by: Jonas Oberhauser Reviewed-by: Alan Stern Acked-by: Andrea Parri Signed-off-by: Paul E. McKenney

tools: memory-model: Add rmw-sequences to the LKMM

2023-01-04T04:47:04+00:00

Viktor (as relayed by Jonas) has pointed out a weakness in the Linux Kernel Memory Model. Namely, the memory ordering properties of atomic operations are not monotonic: An atomic op with full-barrier semantics does not always provide ordering as strong as one with release-barrier semantics. The following litmus test illustrates the problem: -------------------------------------------------- C atomics-not-monotonic {} P0(int *x, atomic_t *y) { WRITE_ONCE(*x, 1); smp_wmb(); atomic_set(y, 1); } P1(atomic_t *y) { int r1; r1 = atomic_inc_return(y); } P2(int *x, atomic_t *y) { int r2; int r3; r2 = atomic_read(y); smp_rmb(); r3 = READ_ONCE(*x); } exists (2:r2=2 /\ 2:r3=0) -------------------------------------------------- The litmus test is allowed as shown with atomic_inc_return(), which has full-barrier semantics. But if the operation is changed to atomic_inc_return_release(), which only has release-barrier semantics, the litmus test is forbidden. Clearly this violates monotonicity. The reason is because the LKMM treats full-barrier atomic ops as if they were written: mb(); load(); store(); mb(); (where the load() and store() are the two parts of an atomic RMW op), whereas it treats release-barrier atomic ops as if they were written: load(); release_barrier(); store(); The difference is that here the release barrier orders the load part of the atomic op before the store part with A-cumulativity, whereas the mb()'s above do not. This means that release-barrier atomics can effectively extend the cumul-fence relation but full-barrier atomics cannot. To resolve this problem we introduce the rmw-sequence relation, representing an arbitrarily long sequence of atomic RMW operations in which each operation reads from the previous one, and explicitly allow it to extend cumul-fence. This modification of the memory model is sound; it holds for PPC because of B-cumulativity, it holds for TSO and ARM64 because of other-multicopy atomicity, and we can assume that atomic ops on all other architectures will be implemented so as to make it hold for them. For similar reasons we also allow rmw-sequence to extend the w-post-bounded relation, which is analogous to cumul-fence in some ways. Reported-by: Viktor Vafeiadis Signed-off-by: Alan Stern Reviewed-by: Jonas Oberhauser Signed-off-by: Paul E. McKenney

tools/memory-model: Provide extra ordering for unlock+lock pair on the same CPU

2021-12-01T01:47:08+00:00

A recent discussion[1] shows that we are in favor of strengthening the ordering of unlock + lock on the same CPU: a unlock and a po-after lock should provide the so-called RCtso ordering, that is a memory access S po-before the unlock should be ordered against a memory access R po-after the lock, unless S is a store and R is a load. The strengthening meets programmers' expection that "sequence of two locked regions to be ordered wrt each other" (from Linus), and can reduce the mental burden when using locks. Therefore add it in LKMM. [1]: https://lore.kernel.org/lkml/20210909185937.GA12379@rowland.harvard.edu/ Co-developed-by: Alan Stern Signed-off-by: Alan Stern Signed-off-by: Boqun Feng Reviewed-by: Michael Ellerman (powerpc) Acked-by: Palmer Dabbelt (RISC-V) Acked-by: Peter Zijlstra (Intel) Signed-off-by: Paul E. McKenney

tools/memory-model: Fix data race detection for unordered store and load

2019-10-05T18:58:14+00:00

Currently the Linux Kernel Memory Model gives an incorrect response for the following litmus test: C plain-WWC {} P0(int *x) { WRITE_ONCE(*x, 2); } P1(int *x, int *y) { int r1; int r2; int r3; r1 = READ_ONCE(*x); if (r1 == 2) { smp_rmb(); r2 = *x; } smp_rmb(); r3 = READ_ONCE(*x); WRITE_ONCE(*y, r3 - 1); } P2(int *x, int *y) { int r4; r4 = READ_ONCE(*y); if (r4 > 0) WRITE_ONCE(*x, 1); } exists (x=2 /\ 1:r2=2 /\ 2:r4=1) The memory model says that the plain read of *x in P1 races with the WRITE_ONCE(*x) in P2. The problem is that we have a write W and a read R related by neither fre or rfe, but rather W ->coe W' ->rfe R, where W' is an intermediate write (the WRITE_ONCE() in P0). In this situation there is no particular ordering between W and R, so either a wr-vis link from W to R or an rw-xbstar link from R to W would prove that the accesses aren't concurrent. But the LKMM only looks for a wr-vis link, which is equivalent to assuming that W must execute before R. This is not necessarily true on non-multicopy-atomic systems, as the WWC pattern demonstrates. This patch changes the LKMM to accept either a wr-vis or a reverse rw-xbstar link as a proof of non-concurrency. Signed-off-by: Alan Stern Acked-by: Andrea Parri Signed-off-by: Paul E. McKenney

tools/memory-model: Improve data-race detection

2019-06-24T16:08:54+00:00

Herbert Xu recently reported a problem concerning RCU and compiler barriers. In the course of discussing the problem, he put forth a litmus test which illustrated a serious defect in the Linux Kernel Memory Model's data-race-detection code [1]. The defect was that the LKMM assumed visibility and executes-before ordering of plain accesses had to be mediated by marked accesses. In Herbert's litmus test this wasn't so, and the LKMM claimed the litmus test was allowed and contained a data race although neither is true. In fact, plain accesses can be ordered by fences even in the absence of marked accesses. In most cases this doesn't matter, because most fences only order accesses within a single thread. But the rcu-fence relation is different; it can order (and induce visibility between) accesses in different threads -- events which otherwise might be concurrent. This makes it relevant to data-race detection. This patch makes two changes to the memory model to incorporate the new insight: If a store is separated by a fence from another access, the store is necessarily visible to the other access (as reflected in the ww-vis and wr-vis relations). Similarly, if a load is separated by a fence from another access then the load necessarily executes before the other access (as reflected in the rw-xbstar relation). If a store is separated by a strong fence from a marked access then it is necessarily visible to any access that executes after the marked access (as reflected in the ww-vis and wr-vis relations). With these changes, the LKMM gives the desired result for Herbert's litmus test and other related ones [2]. [1] https://lore.kernel.org/lkml/Pine.LNX.4.44L0.1906041026570.1731-100000@iolanthe.rowland.org/ [2] https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-1.litmus https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-2.litmus https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-3.litmus https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-4.litmus https://github.com/paulmckrcu/litmus/blob/master/manual/plain/strong-vis.litmus Reported-by: Herbert Xu Signed-off-by: Alan Stern Acked-by: Andrea Parri Signed-off-by: Paul E. McKenney Tested-by: Akira Yokosawa

tools/memory-model: Change definition of rcu-fence

2019-06-21T23:20:49+00:00

The rcu-fence relation in the Linux Kernel Memory Model is not well named. It doesn't act like any other fence relation, in that it does not relate events before a fence to events after that fence. All it does is relate certain RCU events to one another (those that are ordered by the RCU Guarantee); this induces an actual strong-fence-like relation linking events preceding the first RCU event to those following the second. This patch renames rcu-fence, now called rcu-order. It adds a new definition of rcu-fence, something which should have been present all along because it is used in the rb relation. And it modifies the fence and strong-fence relations by making them incorporate the new rcu-fence. As a result of this change, there is no longer any need to define full-fence in the section for detecting data races. It can simply be replaced by the updated strong-fence relation. This change should have no effect on the operation of the memory model. Signed-off-by: Alan Stern Acked-by: Andrea Parri Signed-off-by: Paul E. McKenney