kernel.git/tools/memory-model/Documentation/explanation.txt, branch master

tools/memory-model/Documentation: Fix SRCU section in explanation.txt

2025-04-23T19:17:04Z

The SRCU read-side critical sections describes the difference between srcu_down_read()/srcu_up_read() and srcu_read_lock()/srcu_read_unlock() in a way that a last pair must occur on the same CPU. This is not true, the srcu_read_unlock() can happen on any CPU, but it must be performed by the same task that invoked srcu_read_lock(). Signed-off-by: Uladzislau Rezki (Sony) Signed-off-by: Paul E. McKenney

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

2023-03-22T19:02:21Z

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

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: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: Weaken ctrl dependency definition in explanation.txt

2022-10-18T22:14:52Z

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: Explain syntactic and semantic dependencies

2022-02-02T01:32:30Z

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: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 smp_mb__after_spinlock() spelling

2021-05-10T23:27:20Z

A misspelled git-grep regex revealed that smp_mb__after_spinlock() was misspelled in explanation.txt. This commit adds the missing "_". Fixes: 1c27b644c0fd ("Automate memory-barriers.txt; provide Linux-kernel memory model") [ paulmck: Apply Alan Stern commit-log feedback. ] Signed-off-by: Björn Töpel Signed-off-by: Paul E. McKenney

Merge tag 'locking-core-2020-08-03' of git://git.kernel.org/pub/scm/linux/kernel/git/tip/tip

2020-08-03T21:39:35Z

Pull locking updates from Ingo Molnar: - LKMM updates: mostly documentation changes, but also some new litmus tests for atomic ops. - KCSAN updates: the most important change is that GCC 11 now has all fixes in place to support KCSAN, so GCC support can be enabled again. Also more annotations. - futex updates: minor cleanups and simplifications - seqlock updates: merge preparatory changes/cleanups for the 'associated locks' facilities. - lockdep updates: - simplify IRQ trace event handling - add various new debug checks - simplify header dependencies, split out , decouple lockdep from other low level headers some more - fix NMI handling - misc cleanups and smaller fixes * tag 'locking-core-2020-08-03' of git://git.kernel.org/pub/scm/linux/kernel/git/tip/tip: (60 commits) kcsan: Improve IRQ state trace reporting lockdep: Refactor IRQ trace events fields into struct seqlock: lockdep assert non-preemptibility on seqcount_t write lockdep: Add preemption enabled/disabled assertion APIs seqlock: Implement raw_seqcount_begin() in terms of raw_read_seqcount() seqlock: Add kernel-doc for seqcount_t and seqlock_t APIs seqlock: Reorder seqcount_t and seqlock_t API definitions seqlock: seqcount_t latch: End read sections with read_seqcount_retry() seqlock: Properly format kernel-doc code samples Documentation: locking: Describe seqlock design and usage locking/qspinlock: Do not include atomic.h from qspinlock_types.h locking/atomic: Move ATOMIC_INIT into linux/types.h lockdep: Move list.h inclusion into lockdep.h locking/lockdep: Fix TRACE_IRQFLAGS vs. NMIs futex: Remove unused or redundant includes futex: Consistently use fshared as boolean futex: Remove needless goto's futex: Remove put_futex_key() rwsem: fix commas in initialisation docs: locking: Replace HTTP links with HTTPS ones ...

tools/memory-model: Remove smp_read_barrier_depends() from informal doc

2020-07-21T09:50:37Z

smp_read_barrier_depends() has gone the way of mmiowb() and so many esoteric memory barriers before it. Drop the two mentions of this deceased barrier from the LKMM informal explanation document. Acked-by: Peter Zijlstra (Intel) Acked-by: Alan Stern Acked-by: Paul E. McKenney Signed-off-by: Will Deacon