kernel/linux.git/tools/memory-model/Documentation, branch v6.6.131

Merge tag 'lkmm-scripting.2023.04.07a' of git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu

2023-04-24T19:02:25+00:00

Pull Linux Kernel Memory Model scripting updates from Paul McKenney: "This improves litmus-test documentation and improves the ability to do before/after tests on the https://github.com/paulmckrcu/litmus repo" * tag 'lkmm-scripting.2023.04.07a' of git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu: (32 commits) tools/memory-model: Remove out-of-date SRCU documentation tools/memory-model: Document LKMM test procedure tools/memory-model: Use "grep -E" instead of "egrep" tools/memory-model: Use "-unroll 0" to keep --hw runs finite tools/memory-model: Make judgelitmus.sh handle scripted Result: tag tools/memory-model: Add data-race capabilities to judgelitmus.sh tools/memory-model: Add checktheselitmus.sh to run specified litmus tests tools/memory-model: Repair parseargs.sh header comment tools/memory-model: Add "--" to parseargs.sh for additional arguments tools/memory-model: Make history-check scripts use mselect7 tools/memory-model: Make checkghlitmus.sh use mselect7 tools/memory-model: Fix scripting --jobs argument tools/memory-model: Implement --hw support for checkghlitmus.sh tools/memory-model: Add -v flag to jingle7 runs tools/memory-model: Make runlitmus.sh check for jingle errors tools/memory-model: Allow herd to deduce CPU type tools/memory-model: Keep assembly-language litmus tests tools/memory-model: Move from .AArch64.litmus.out to .litmus.AArch.out tools/memory-model: Make runlitmus.sh generate .litmus.out for --hw tools/memory-model: Split runlitmus.sh out of checklitmus.sh ...

tools/memory-model: Remove out-of-date SRCU documentation

2023-03-24T17:24:48+00:00

Commit 6cd244c87428 ("tools/memory-model: Provide exact SRCU semantics") changed the semantics of partially overlapping SRCU read-side critical sections (among other things), making such documentation out-of-date. The new, semantic changes are discussed in explanation.txt. Remove the out-of-date documentation. Signed-off-by: Andrea Parri Reviewed-by: Joel Fernandes (Google) Acked-by: Alan Stern Signed-off-by: Paul E. McKenney

tools/memory-model: Document locking corner cases

2023-03-24T17:22:25+00:00

Most Linux-kernel uses of locking are straightforward, but there are corner-case uses that rely on less well-known aspects of the lock and unlock primitives. This commit therefore adds a locking.txt and litmus tests in Documentation/litmus-tests/locking to explain these corner-case uses. [ paulmck: Apply Andrea Parri feedback for klitmus7. ] [ paulmck: Apply Akira Yokosawa example-consistency feedback. ] Reviewed-by: Akira Yokosawa Signed-off-by: Paul E. McKenney

tools/memory-model: Add documentation about SRCU read-side critical sections

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

Expand the discussion of SRCU and its read-side critical sections in the Linux Kernel Memory Model documentation file explanation.txt. The new material discusses recent changes to the memory model made in commit 6cd244c87428 ("tools/memory-model: Provide exact SRCU semantics"). Signed-off-by: Alan Stern Co-developed-by: Joel Fernandes (Google) Signed-off-by: Joel Fernandes (Google) Reviewed-by: Akira Yokosawa Cc: Andrea Parri Cc: Boqun Feng Cc: Jade Alglave Cc: Jonas Oberhauser Cc: Luc Maranget Cc: "Paul E. McKenney" Cc: Peter Zijlstra CC: Will Deacon 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 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: Weaken ctrl dependency definition in explanation.txt

2022-10-18T22:14:52+00:00

The current informal control dependency definition in explanation.txt is too broad and, as discussed, needs to be updated. Consider the following example: > if(READ_ONCE(x)) > return 42; > > WRITE_ONCE(y, 42); > > return 21; The read event determines whether the write event will be executed "at all" - as per the current definition - but the formal LKMM does not recognize this as a control dependency. Introduce a new definition which includes the requirement for the second memory access event to syntactically lie within the arm of a non-loop conditional. Link: https://lore.kernel.org/all/20220615114330.2573952-1-paul.heidekrueger@in.tum.de/ Cc: Marco Elver Cc: Charalampos Mainas Cc: Pramod Bhatotia Cc: Soham Chakraborty Cc: Martin Fink Co-developed-by: Alan Stern Signed-off-by: Alan Stern Signed-off-by: Paul Heidekrüger Signed-off-by: Paul E. McKenney

tools/memory-model: Clarify LKMM's limitations in litmus-tests.txt

2022-08-31T12:15:31+00:00

As discussed, clarify LKMM not recognizing certain kinds of orderings. In particular, highlight the fact that LKMM might deliberately make weaker guarantees than compilers and architectures. [ paulmck: Fix whitespace issue noted by checkpatch.pl. ] Link: https://lore.kernel.org/all/YpoW1deb%2FQeeszO1@ethstick13.dse.in.tum.de/T/#u Co-developed-by: Alan Stern Signed-off-by: Alan Stern Signed-off-by: Paul Heidekrüger Reviewed-by: Marco Elver Reviewed-by: Joel Fernandes (Google) Cc: Charalampos Mainas Cc: Pramod Bhatotia Cc: Soham Chakraborty Cc: Martin Fink Signed-off-by: Paul E. McKenney

tools/memory-model: Explain syntactic and semantic dependencies

2022-02-02T01:32:30+00:00

Paul Heidekrüger pointed out that the Linux Kernel Memory Model documentation doesn't mention the distinction between syntactic and semantic dependencies. This is an important difference, because the compiler can easily break dependencies that are only syntactic, not semantic. This patch adds a few paragraphs to the LKMM documentation explaining these issues and illustrating how they can matter. Suggested-by: Paul Heidekrüger Reviewed-by: Akira Yokosawa Signed-off-by: Alan Stern 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