From e8adbac0d44fe5f275902c004d04b0cfc33fce8d Mon Sep 17 00:00:00 2001 From: Andrea Parri Date: Wed, 19 Jun 2024 03:06:04 +0200 Subject: [PATCH 1/5] tools/memory-model: Document herd7 (abstract) representation The Linux-kernel memory model (LKMM) source code and the herd7 tool are closely linked in that the latter is responsible for (pre)processing each C-like macro of a litmus test, and for providing the LKMM with a set of events, or "representation", corresponding to the given macro. This commit therefore provides herd-representation.txt to document the representations of the concurrency macros, following their "classification" in Documentation/atomic_t.txt. Link: https://lore.kernel.org/all/ZnFZPJlILp5B9scN@andrea/ Suggested-by: Hernan Ponce de Leon Signed-off-by: Andrea Parri Reviewed-by: Boqun Feng Reviewed-by: Hernan Ponce de Leon Signed-off-by: Paul E. McKenney --- tools/memory-model/Documentation/README | 7 +- .../Documentation/herd-representation.txt | 110 ++++++++++++++++++ 2 files changed, 116 insertions(+), 1 deletion(-) create mode 100644 tools/memory-model/Documentation/herd-representation.txt diff --git a/tools/memory-model/Documentation/README b/tools/memory-model/Documentation/README index 304162743a5b..44e7dae73b29 100644 --- a/tools/memory-model/Documentation/README +++ b/tools/memory-model/Documentation/README @@ -33,7 +33,8 @@ o You are familiar with Linux-kernel concurrency and the use of o You are familiar with Linux-kernel concurrency and the use of LKMM, and would like to learn about LKMM's requirements, - rationale, and implementation: explanation.txt + rationale, and implementation: explanation.txt and + herd-representation.txt o You are interested in the publications related to LKMM, including hardware manuals, academic literature, standards-committee @@ -61,6 +62,10 @@ control-dependencies.txt explanation.txt Detailed description of the memory model. +herd-representation.txt + The (abstract) representation of the Linux-kernel concurrency + primitives in terms of events. + litmus-tests.txt The format, features, capabilities, and limitations of the litmus tests that LKMM can evaluate. diff --git a/tools/memory-model/Documentation/herd-representation.txt b/tools/memory-model/Documentation/herd-representation.txt new file mode 100644 index 000000000000..ed988906f2b7 --- /dev/null +++ b/tools/memory-model/Documentation/herd-representation.txt @@ -0,0 +1,110 @@ +# +# Legend: +# R, a Load event +# W, a Store event +# F, a Fence event +# LKR, a Lock-Read event +# LKW, a Lock-Write event +# UL, an Unlock event +# LF, a Lock-Fail event +# RL, a Read-Locked event +# RU, a Read-Unlocked event +# R*, a Load event included in RMW +# W*, a Store event included in RMW +# SRCU, a Sleepable-Read-Copy-Update event +# +# po, a Program-Order link +# rmw, a Read-Modify-Write link - every rmw link is a po link +# +# By convention, a blank line in a cell means "same as the preceding line". +# +# Disclaimer. The table includes representations of "add" and "and" operations; +# corresponding/identical representations of "sub", "inc", "dec" and "or", "xor", +# "andnot" operations are omitted. +# + ------------------------------------------------------------------------------ + | C macro | Events | + ------------------------------------------------------------------------------ + | Non-RMW ops | | + ------------------------------------------------------------------------------ + | READ_ONCE | R[once] | + | atomic_read | | + | WRITE_ONCE | W[once] | + | atomic_set | | + | smp_load_acquire | R[acquire] | + | atomic_read_acquire | | + | smp_store_release | W[release] | + | atomic_set_release | | + | smp_store_mb | W[once] ->po F[mb] | + | smp_mb | F[mb] | + | smp_rmb | F[rmb] | + | smp_wmb | F[wmb] | + | smp_mb__before_atomic | F[before-atomic] | + | smp_mb__after_atomic | F[after-atomic] | + | spin_unlock | UL | + | spin_is_locked | On success: RL | + | | On failure: RU | + | smp_mb__after_spinlock | F[after-spinlock] | + | smp_mb__after_unlock_lock | F[after-unlock-lock] | + | rcu_read_lock | F[rcu-lock] | + | rcu_read_unlock | F[rcu-unlock] | + | synchronize_rcu | F[sync-rcu] | + | rcu_dereference | R[once] | + | rcu_assign_pointer | W[release] | + | srcu_read_lock | R[srcu-lock] | + | srcu_down_read | | + | srcu_read_unlock | W[srcu-unlock] | + | srcu_up_read | | + | synchronize_srcu | SRCU[sync-srcu] | + | smp_mb__after_srcu_read_unlock | F[after-srcu-read-unlock] | + ------------------------------------------------------------------------------ + | RMW ops w/o return value | | + ------------------------------------------------------------------------------ + | atomic_add | R*[noreturn] ->rmw W*[once] | + | atomic_and | | + | spin_lock | LKR ->po LKW | + ------------------------------------------------------------------------------ + | RMW ops w/ return value | | + ------------------------------------------------------------------------------ + | atomic_add_return | F[mb] ->po R*[once] | + | | ->rmw W*[once] ->po F[mb] | + | atomic_fetch_add | | + | atomic_fetch_and | | + | atomic_xchg | | + | xchg | | + | atomic_add_negative | | + | atomic_add_return_relaxed | R*[once] ->rmw W*[once] | + | atomic_fetch_add_relaxed | | + | atomic_fetch_and_relaxed | | + | atomic_xchg_relaxed | | + | xchg_relaxed | | + | atomic_add_negative_relaxed | | + | atomic_add_return_acquire | R*[acquire] ->rmw W*[once] | + | atomic_fetch_add_acquire | | + | atomic_fetch_and_acquire | | + | atomic_xchg_acquire | | + | xchg_acquire | | + | atomic_add_negative_acquire | | + | atomic_add_return_release | R*[once] ->rmw W*[release] | + | atomic_fetch_add_release | | + | atomic_fetch_and_release | | + | atomic_xchg_release | | + | xchg_release | | + | atomic_add_negative_release | | + ------------------------------------------------------------------------------ + | Conditional RMW ops | | + ------------------------------------------------------------------------------ + | atomic_cmpxchg | On success: F[mb] ->po R*[once] | + | | ->rmw W*[once] ->po F[mb] | + | | On failure: R*[once] | + | cmpxchg | | + | atomic_add_unless | | + | atomic_cmpxchg_relaxed | On success: R*[once] ->rmw W*[once] | + | | On failure: R*[once] | + | atomic_cmpxchg_acquire | On success: R*[acquire] ->rmw W*[once] | + | | On failure: R*[once] | + | atomic_cmpxchg_release | On success: R*[once] ->rmw W*[release] | + | | On failure: R*[once] | + | spin_trylock | On success: LKR ->po LKW | + | | On failure: LF | + ------------------------------------------------------------------------------ From 9bc931e9e161ca9788ebed1d2a88b5aa1b4439b2 Mon Sep 17 00:00:00 2001 From: Akira Yokosawa Date: Tue, 25 Jun 2024 17:58:21 +0900 Subject: [PATCH 2/5] tools/memory-model: Add locking.txt and glossary.txt to README locking.txt and glossary.txt have been in LKMM's documentation for quite a while. Add them in README's introduction of docs and the list of docs at the bottom. Add access-marking.txt in the former as well. Signed-off-by: Akira Yokosawa Acked-by: Andrea Parri Cc: Marco Elver Signed-off-by: Paul E. McKenney --- tools/memory-model/Documentation/README | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/tools/memory-model/Documentation/README b/tools/memory-model/Documentation/README index 44e7dae73b29..9999c1effdb6 100644 --- a/tools/memory-model/Documentation/README +++ b/tools/memory-model/Documentation/README @@ -9,6 +9,8 @@ depending on what you know and what you would like to learn. Please note that the documents later in this list assume that the reader understands the material provided by documents earlier in this list. +If LKMM-specific terms lost you, glossary.txt might help you. + o You are new to Linux-kernel concurrency: simple.txt o You have some background in Linux-kernel concurrency, and would @@ -21,6 +23,9 @@ o You are familiar with the Linux-kernel concurrency primitives that you need, and just want to get started with LKMM litmus tests: litmus-tests.txt +o You would like to access lock-protected shared variables without + having their corresponding locks held: locking.txt + o You are familiar with Linux-kernel concurrency, and would like a detailed intuitive understanding of LKMM, including situations involving more than two threads: recipes.txt @@ -28,6 +33,11 @@ o You are familiar with Linux-kernel concurrency, and would o You would like a detailed understanding of what your compiler can and cannot do to control dependencies: control-dependencies.txt +o You would like to mark concurrent normal accesses to shared + variables so that intentional "racy" accesses can be properly + documented, especially when you are responding to complaints + from KCSAN: access-marking.txt + o You are familiar with Linux-kernel concurrency and the use of LKMM, and would like a quick reference: cheatsheet.txt @@ -62,6 +72,9 @@ control-dependencies.txt explanation.txt Detailed description of the memory model. +glossary.txt + Brief definitions of LKMM-related terms. + herd-representation.txt The (abstract) representation of the Linux-kernel concurrency primitives in terms of events. @@ -70,6 +83,10 @@ litmus-tests.txt The format, features, capabilities, and limitations of the litmus tests that LKMM can evaluate. +locking.txt + Rules for accessing lock-protected shared variables outside of + their corresponding critical sections. + ordering.txt Overview of the Linux kernel's low-level memory-ordering primitives by category. From b9a6e87af5eaf4239a11ebc029d59e8ace761f1f Mon Sep 17 00:00:00 2001 From: Akira Yokosawa Date: Tue, 25 Jun 2024 17:59:37 +0900 Subject: [PATCH 3/5] tools/memory-model: simple.txt: Fix stale reference to recipes-pairs.txt There has never been recipes-paris.txt at least since v5.11. Fix the typo. Signed-off-by: Akira Yokosawa Acked-by: Andrea Parri Signed-off-by: Paul E. McKenney --- tools/memory-model/Documentation/simple.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/memory-model/Documentation/simple.txt b/tools/memory-model/Documentation/simple.txt index 4c789ec8334f..21f06c1d1b70 100644 --- a/tools/memory-model/Documentation/simple.txt +++ b/tools/memory-model/Documentation/simple.txt @@ -266,5 +266,5 @@ More complex use cases ====================== If the alternatives above do not do what you need, please look at the -recipes-pairs.txt file to peel off the next layer of the memory-ordering +recipes.txt file to peel off the next layer of the memory-ordering onion. From 2040c9cb140ec2925be9c6c18479d796ced15126 Mon Sep 17 00:00:00 2001 From: Akira Yokosawa Date: Tue, 2 Jul 2024 20:42:44 +0900 Subject: [PATCH 4/5] docs/memory-barriers.txt: Remove left-over references to "CACHE COHERENCY" Commit 8ca924aeb4f2 ("Documentation/barriers: Remove references to [smp_]read_barrier_depends()") removed the entire section of "CACHE COHERENCY", without getting rid of its traces. Remove them. Signed-off-by: Akira Yokosawa Cc: Will Deacon Signed-off-by: Paul E. McKenney Acked-by: Andrea Parri --- Documentation/memory-barriers.txt | 3 --- 1 file changed, 3 deletions(-) diff --git a/Documentation/memory-barriers.txt b/Documentation/memory-barriers.txt index 4202174a6262..93d58d9a428b 100644 --- a/Documentation/memory-barriers.txt +++ b/Documentation/memory-barriers.txt @@ -88,7 +88,6 @@ CONTENTS (*) The effects of the cpu cache. - - Cache coherency. - Cache coherency vs DMA. - Cache coherency vs MMIO. @@ -677,8 +676,6 @@ include/linux/rcupdate.h. This permits the current target of an RCU'd pointer to be replaced with a new modified target, without the replacement target appearing to be incompletely initialised. -See also the subsection on "Cache Coherency" for a more thorough example. - CONTROL DEPENDENCIES -------------------- From a49f48cc7d26270bee727d30ce830d4129b33d4a Mon Sep 17 00:00:00 2001 From: Boqun Feng Date: Wed, 3 Jul 2024 09:26:16 -0700 Subject: [PATCH 5/5] MAINTAINERS: Add the dedicated maillist info for LKMM A dedicated mail list has been created for Linux kernel memory model discussion, which could help people more easily track memory model related discussions. This could also help bring memory model discussions to a broader audience. Therefore, add the list information to the LKMM maintainers entry. Signed-off-by: Boqun Feng Signed-off-by: Paul E. McKenney Acked-by: Andrea Parri --- MAINTAINERS | 1 + 1 file changed, 1 insertion(+) diff --git a/MAINTAINERS b/MAINTAINERS index 42decde38320..0a3a769148fd 100644 --- a/MAINTAINERS +++ b/MAINTAINERS @@ -12993,6 +12993,7 @@ R: Daniel Lustig R: Joel Fernandes L: linux-kernel@vger.kernel.org L: linux-arch@vger.kernel.org +L: lkmm@lists.linux.dev S: Supported T: git git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu.git dev F: Documentation/atomic_bitops.txt