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

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

2023-01-04T04:47:04Z

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:08Z

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:14Z

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:54Z

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:49Z

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

tools/memory-model: Expand definition of barrier

2019-06-21T23:18:45Z

Commit 66be4e66a7f4 ("rcu: locking and unlocking need to always be at least barriers") added compiler barriers back into rcu_read_lock() and rcu_read_unlock(). Furthermore, srcu_read_lock() and srcu_read_unlock() have always contained compiler barriers. The Linux Kernel Memory Model ought to know about these barriers. This patch adds them into the memory model. Signed-off-by: Alan Stern Acked-by: Andrea Parri Signed-off-by: Paul E. McKenney

tools/memory-model: Add data-race detection

2019-05-28T15:18:21Z

This patch adds data-race detection to the Linux-Kernel Memory Model. As part of this effort, support is added for: compiler barriers (the barrier() function), and a new Preserved Program Order term: (addr ; [Plain] ; wmb) Data races are marked with a special Flag warning in herd. It is not guaranteed that the model will provide accurate predictions when a data race is present. The patch does not include documentation for the data-race detection facility. The basic design has been explained in various emails, and a separate documentation patch will be submitted later. This work is based on an earlier formulation of data races for the LKMM by Andrea Parri. Signed-off-by: Alan Stern Reviewed-by: Andrea Parri Signed-off-by: Paul E. McKenney

tools/memory-model: Add definitions of plain and marked accesses

2019-05-28T15:18:21Z

This patch adds definitions for marked and plain accesses to the Linux-Kernel Memory Model. It also modifies the definitions of the existing parts of the model (including the cumul-fence, prop, hb, pb, and rb relations) so as to make them apply only to marked accesses. Signed-off-by: Alan Stern Reviewed-by: Andrea Parri Signed-off-by: Paul E. McKenney

tools/memory-model: Prepare for data-race detection

2019-05-28T15:18:21Z

This patch makes some slight alterations to linux-kernel.cat in preparation for adding support for data-race detection to the Linux-Kernel Memory Model. The definitions of relations involved in Acquire, Release, and unlock-lock ordering are moved up earlier in the source file. The rmb relation is factored through the new R4rmb class: the class of reads to which rmb will apply. The definition of the fence relation is moved earlier, and it is split up into read- and write-fences (rmb and wmb) and all the others. This should not make any functional changes. Signed-off-by: Alan Stern Reviewed-by: Andrea Parri Signed-off-by: Paul E. McKenney

tools/memory-model: Avoid duplicating herdtools versions

2019-03-18T17:27:52Z

Currently, herdtools version information appears no fewer than three times in the LKMM source, which is difficult to maintain. This commit therefore places the required version in one place, namely the tools/memory-model/README file. Signed-off-by: Andrea Parri Signed-off-by: Paul E. McKenney Acked-by: Alan Stern