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

tools/memory-model: Distinguish between syntactic and semantic tags

2025-02-25T18:17:39+00:00

Not all annotated accesses provide the semantics their syntactic tags would imply. For example, an 'acquire tag on a write does not imply that the write is finally in the Acquire set and provides acquire ordering. To distinguish in those cases between the syntactic tags and actual sets, we capitalize the former, so 'ACQUIRE tags may be present on both reads and writes, but only reads will appear in the Acquire set. For tags where the two concepts are the same we do not use specific capitalization to make this distinction. Reported-by: Boqun Feng Signed-off-by: Jonas Oberhauser Reviewed-by: Boqun Feng Tested-by: Boqun Feng Signed-off-by: Paul E. McKenney Tested-by: Akira Yokosawa # herdtools7.7.58

tools/memory-model: Switch to softcoded herd7 tags

2025-02-25T18:16:57+00:00

A new version of herd7 provides a -lkmmv2 switch which overrides the old herd7 behavior of simply ignoring any softcoded tags in the .def and .bell files. We port LKMM to this version of herd7 by providing the switch in linux-kernel.cfg and reporting an error if the LKMM is used without this switch. To preserve the semantics of LKMM, we also softcode the Noreturn tag on atomic RMW which do not return a value and define atomic_add_unless with an Mb tag in linux-kernel.def. We update the herd-representation.txt accordingly and clarify some of the resulting combinations. Co-developed-by: Hernan Ponce de Leon Signed-off-by: Hernan Ponce de Leon Signed-off-by: Jonas Oberhauser Signed-off-by: Paul E. McKenney Reviewed-by: Boqun Feng Tested-by: Boqun Feng Tested-by: Akira Yokosawa # herdtools7.7.58

tools/memory-model: Define applicable tags on operation in tools/...

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

Herd7 transforms reads, writes, and read-modify-writes by eliminating 'acquire tags from writes, 'release tags from reads, and 'acquire, 'release, and 'mb tags from failed read-modify-writes. We emulate this behavior by redefining Acquire, Release, and Mb sets in linux-kernel.bell to explicitly exclude those combinations. Herd7 furthermore adds 'noreturn tag to certain reads. Currently herd7 does not allow specifying the 'noreturn tag manually, but such manual declaration (e.g., through a syntax __atomic_op{noreturn}) would add invalid 'noreturn tags to writes; in preparation, we already also exclude this combination. Signed-off-by: Jonas Oberhauser Signed-off-by: Paul E. McKenney Reviewed-by: Boqun Feng Tested-by: Boqun Feng

tools/memory-model: Legitimize current use of tags in LKMM macros

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

The current macros in linux-kernel.def reference instructions such as __xchg{mb} or __cmpxchg{acquire}, which are invalid combinations of tags and instructions according to the declarations in linux-kernel.bell. This works with current herd7 because herd7 removes these tags anyways and does not actually enforce validity of combinations at all. If a future herd7 version no longer applies these hardcoded transformations, then all currently invalid combinations will actually appear on some instruction. We therefore adjust the declarations to make the resulting combinations valid, by adding the 'mb tag to the set of Accesses and allowing all Accesses to appear on all read, write, and RMW instructions. Signed-off-by: Jonas Oberhauser Signed-off-by: Paul E. McKenney Reviewed-by: Boqun Feng Tested-by: Boqun Feng

tools/memory-model: Provide exact SRCU semantics

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

LKMM has long provided only approximate handling of SRCU read-side critical sections. This has not been a pressing problem because LKMM's traditional handling is correct for the common cases of non-overlapping and properly nested critical sections. However, LKMM's traditional handling of partially overlapping critical sections incorrectly fuses them into one large critical section. For example, consider the following litmus test: ------------------------------------------------------------------------ C C-srcu-nest-5 (* * Result: Sometimes * * This demonstrates non-nested overlapping of SRCU read-side critical * sections. Unlike RCU, SRCU critical sections do not unconditionally * nest. *) {} P0(int *x, int *y, struct srcu_struct *s1) { int r1; int r2; int r3; int r4; r3 = srcu_read_lock(s1); r2 = READ_ONCE(*y); r4 = srcu_read_lock(s1); srcu_read_unlock(s1, r3); r1 = READ_ONCE(*x); srcu_read_unlock(s1, r4); } P1(int *x, int *y, struct srcu_struct *s1) { WRITE_ONCE(*y, 1); synchronize_srcu(s1); WRITE_ONCE(*x, 1); } locations [0:r1] exists (0:r1=1 /\ 0:r2=0) ------------------------------------------------------------------------ Current mainline incorrectly flattens the two critical sections into one larger critical section, giving "Never" instead of the correct "Sometimes": ------------------------------------------------------------------------ $ herd7 -conf linux-kernel.cfg C-srcu-nest-5.litmus Test C-srcu-nest-5 Allowed States 3 0:r1=0; 0:r2=0; 0:r1=0; 0:r2=1; 0:r1=1; 0:r2=1; No Witnesses Positive: 0 Negative: 3 Flag srcu-bad-nesting Condition exists (0:r1=1 /\ 0:r2=0) Observation C-srcu-nest-5 Never 0 3 Time C-srcu-nest-5 0.01 Hash=e692c106cf3e84e20f12991dc438ff1b ------------------------------------------------------------------------ To its credit, it does complain about bad nesting. But with this commit we get the following result, which has the virtue of being correct: ------------------------------------------------------------------------ $ herd7 -conf linux-kernel.cfg C-srcu-nest-5.litmus Test C-srcu-nest-5 Allowed States 4 0:r1=0; 0:r2=0; 0:r1=0; 0:r2=1; 0:r1=1; 0:r2=0; 0:r1=1; 0:r2=1; Ok Witnesses Positive: 1 Negative: 3 Condition exists (0:r1=1 /\ 0:r2=0) Observation C-srcu-nest-5 Sometimes 1 3 Time C-srcu-nest-5 0.05 Hash=e692c106cf3e84e20f12991dc438ff1b ------------------------------------------------------------------------ In addition, there are new srcu_down_read() and srcu_up_read() functions on their way to mainline. Roughly speaking, these are to srcu_read_lock() and srcu_read_unlock() as down() and up() are to mutex_lock() and mutex_unlock(). The key point is that srcu_down_read() can execute in one process and the matching srcu_up_read() in another, as shown in this litmus test: ------------------------------------------------------------------------ C C-srcu-nest-6 (* * Result: Never * * This would be valid for srcu_down_read() and srcu_up_read(). *) {} P0(int *x, int *y, struct srcu_struct *s1, int *idx, int *f) { int r2; int r3; r3 = srcu_down_read(s1); WRITE_ONCE(*idx, r3); r2 = READ_ONCE(*y); smp_store_release(f, 1); } P1(int *x, int *y, struct srcu_struct *s1, int *idx, int *f) { int r1; int r3; int r4; r4 = smp_load_acquire(f); r1 = READ_ONCE(*x); r3 = READ_ONCE(*idx); srcu_up_read(s1, r3); } P2(int *x, int *y, struct srcu_struct *s1) { WRITE_ONCE(*y, 1); synchronize_srcu(s1); WRITE_ONCE(*x, 1); } locations [0:r1] filter (1:r4=1) exists (1:r1=1 /\ 0:r2=0) ------------------------------------------------------------------------ When run on current mainline, this litmus test gets a complaint about an unknown macro srcu_down_read(). With this commit: ------------------------------------------------------------------------ herd7 -conf linux-kernel.cfg C-srcu-nest-6.litmus Test C-srcu-nest-6 Allowed States 3 0:r1=0; 0:r2=0; 1:r1=0; 0:r1=0; 0:r2=1; 1:r1=0; 0:r1=0; 0:r2=1; 1:r1=1; No Witnesses Positive: 0 Negative: 3 Condition exists (1:r1=1 /\ 0:r2=0) Observation C-srcu-nest-6 Never 0 3 Time C-srcu-nest-6 0.02 Hash=c1f20257d052ca5e899be508bedcb2a1 ------------------------------------------------------------------------ Note that the user must supply the flag "f" and the "filter" clause, similar to what must be done to emulate call_rcu(). The commit works by treating srcu_read_lock()/srcu_down_read() as loads and srcu_read_unlock()/srcu_up_read() as stores. This allows us to determine which unlock matches which lock by looking for a data dependency between them. In order for this to work properly, the data dependencies have to be tracked through stores to intermediate variables such as "idx" in the litmus test above; this is handled by the new carry-srcu-data relation. But it's important here (and in the existing carry-dep relation) to avoid tracking the dependencies through SRCU unlock stores. Otherwise, in situations resembling: A: r1 = srcu_read_lock(s); B: srcu_read_unlock(s, r1); C: r2 = srcu_read_lock(s); D: srcu_read_unlock(s, r2); it would look as if D was dependent on both A and C, because "s" would appear to be an intermediate variable written by B and read by C. This explains the complications in the definitions of carry-srcu-dep and carry-dep. As a debugging aid, the commit adds a check for errors in which the value returned by one call to srcu_read_lock()/srcu_down_read() is passed to more than one instance of srcu_read_unlock()/srcu_up_read(). Finally, since these SRCU-related primitives are now treated as ordinary reads and writes, we have to add them into the lists of marked accesses (i.e., not subject to data races) and lock-related accesses (i.e., one shouldn't try to access an srcu_struct with a non-lock-related primitive such as READ_ONCE() or a plain write). Portions of this approach were suggested by Boqun Feng and Jonas Oberhauser. [ paulmck: Fix space-before-tab whitespace nit. ] Reported-by: Paul E. McKenney Signed-off-by: Alan Stern Reviewed-by: Jonas Oberhauser 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: Update some warning labels

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

Some of the warning labels used in the LKMM are unfortunately ambiguous. In particular, the same warning is used for both an unmatched rcu_read_lock() call and for an unmatched rcu_read_unlock() call. Likewise for the srcu_* equivalents. Also, the warning about passing a wrong value to srcu_read_unlock() -- i.e., a value different from the one returned by the matching srcu_read_lock() -- talks about bad nesting rather than non-matching values. Let's update the warning labels to make their meanings more clear. Signed-off-by: Alan Stern Reviewed-by: Jonas Oberhauser Acked-by: Andrea Parri Signed-off-by: Paul E. McKenney

tools: memory-model: Make plain accesses carry dependencies

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

As reported by Viktor, plain accesses in LKMM are weaker than accesses to registers: the latter carry dependencies but the former do not. This is exemplified in the following snippet: int r = READ_ONCE(*x); WRITE_ONCE(*y, r); Here a data dependency links the READ_ONCE() to the WRITE_ONCE(), preserving their order, because the model treats r as a register. If r is turned into a memory location accessed by plain accesses, however, the link is broken and the order between READ_ONCE() and WRITE_ONCE() is no longer preserved. This is too conservative, since any optimizations on plain accesses that might break dependencies are also possible on registers; it also contradicts the intuitive notion of "dependency" as the data stored by the WRITE_ONCE() does depend on the data read by the READ_ONCE(), independently of whether r is a register or a memory location. This is resolved by redefining all dependencies to include dependencies carried by memory accesses; a dependency is said to be carried by memory accesses (in the model: carry-dep) from one load to another load if the initial load is followed by an arbitrarily long sequence alternating between stores and loads of the same thread, where the data of each store depends on the previous load, and is read by the next load. Any dependency linking the final load in the sequence to another access also links the initial load in the sequence to that access. More deep details can be found in this LKML discussion: https://lore.kernel.org/lkml/d86295788ad14a02874ab030ddb8a6f8@huawei.com/ Reported-by: Viktor Vafeiadis Signed-off-by: Jonas Oberhauser Reviewed-by: Alan Stern Signed-off-by: Paul E. McKenney

tools/memory-model: Add data-race detection

2019-05-28T15:18:21+00:00

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:21+00:00

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