From 2ada0addbdb68387074a72fe5530e5d49da9a147 Mon Sep 17 00:00:00 2001 From: Puranjay Mohan Date: Wed, 8 May 2024 14:34:00 +0000 Subject: tools/memory-model: Add atomic_and()/or()/xor() and add_negative Pull-849[1] added the support of '&', '|', and '^' to the herd7 tool's atomics operations. Use these in linux-kernel.def to implement atomic_and()/or()/xor() with all their ordering variants. atomic_add_negative() is already available so add its acquire, release, and relaxed ordering variants. [1] https://github.com/herd/herdtools7/pull/849 Signed-off-by: Puranjay Mohan Acked-by: Andrea Parri Reviewed-by: Boqun Feng Signed-off-by: Paul E. McKenney Cc: Alan Stern Cc: Will Deacon Cc: Peter Zijlstra Cc: Nicholas Piggin Cc: David Howells Cc: Jade Alglave Cc: Luc Maranget Cc: Akira Yokosawa Cc: Daniel Lustig Cc: Joel Fernandes Cc: --- tools/memory-model/linux-kernel.def | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) (limited to 'tools') diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def index 88a39601f525..d1f11930ec51 100644 --- a/tools/memory-model/linux-kernel.def +++ b/tools/memory-model/linux-kernel.def @@ -65,6 +65,9 @@ atomic_set_release(X,V) { smp_store_release(X,V); } atomic_add(V,X) { __atomic_op(X,+,V); } atomic_sub(V,X) { __atomic_op(X,-,V); } +atomic_and(V,X) { __atomic_op(X,&,V); } +atomic_or(V,X) { __atomic_op(X,|,V); } +atomic_xor(V,X) { __atomic_op(X,^,V); } atomic_inc(X) { __atomic_op(X,+,1); } atomic_dec(X) { __atomic_op(X,-,1); } @@ -77,6 +80,21 @@ atomic_fetch_add_relaxed(V,X) __atomic_fetch_op{once}(X,+,V) atomic_fetch_add_acquire(V,X) __atomic_fetch_op{acquire}(X,+,V) atomic_fetch_add_release(V,X) __atomic_fetch_op{release}(X,+,V) +atomic_fetch_and(V,X) __atomic_fetch_op{mb}(X,&,V) +atomic_fetch_and_relaxed(V,X) __atomic_fetch_op{once}(X,&,V) +atomic_fetch_and_acquire(V,X) __atomic_fetch_op{acquire}(X,&,V) +atomic_fetch_and_release(V,X) __atomic_fetch_op{release}(X,&,V) + +atomic_fetch_or(V,X) __atomic_fetch_op{mb}(X,|,V) +atomic_fetch_or_relaxed(V,X) __atomic_fetch_op{once}(X,|,V) +atomic_fetch_or_acquire(V,X) __atomic_fetch_op{acquire}(X,|,V) +atomic_fetch_or_release(V,X) __atomic_fetch_op{release}(X,|,V) + +atomic_fetch_xor(V,X) __atomic_fetch_op{mb}(X,^,V) +atomic_fetch_xor_relaxed(V,X) __atomic_fetch_op{once}(X,^,V) +atomic_fetch_xor_acquire(V,X) __atomic_fetch_op{acquire}(X,^,V) +atomic_fetch_xor_release(V,X) __atomic_fetch_op{release}(X,^,V) + atomic_inc_return(X) __atomic_op_return{mb}(X,+,1) atomic_inc_return_relaxed(X) __atomic_op_return{once}(X,+,1) atomic_inc_return_acquire(X) __atomic_op_return{acquire}(X,+,1) @@ -117,3 +135,6 @@ atomic_sub_and_test(V,X) __atomic_op_return{mb}(X,-,V) == 0 atomic_dec_and_test(X) __atomic_op_return{mb}(X,-,1) == 0 atomic_inc_and_test(X) __atomic_op_return{mb}(X,+,1) == 0 atomic_add_negative(V,X) __atomic_op_return{mb}(X,+,V) < 0 +atomic_add_negative_relaxed(V,X) __atomic_op_return{once}(X,+,V) < 0 +atomic_add_negative_acquire(V,X) __atomic_op_return{acquire}(X,+,V) < 0 +atomic_add_negative_release(V,X) __atomic_op_return{release}(X,+,V) < 0 -- cgit v1.2.3 From e176ebffc3f4a18b79f295fd9c322e936bc14592 Mon Sep 17 00:00:00 2001 From: Puranjay Mohan Date: Tue, 14 May 2024 09:46:33 +0000 Subject: tools/memory-model: Add atomic_andnot() with its variants Pull-855[1] added the support of atomic_andnot() to the herd tool. Use this to add the implementation in the LKMM. All of the ordering variants are also added. Here is a small litmus-test that uses this operation: C andnot { atomic_t u = ATOMIC_INIT(7); } P0(atomic_t *u) { r0 = atomic_fetch_andnot(3, u); r1 = READ_ONCE(*u); } exists (0:r0=7 /\ 0:r1=4) Test andnot Allowed States 1 0:r0=7; 0:r1=4; Ok Witnesses Positive: 1 Negative: 0 Condition exists (0:r0=7 /\ 0:r1=4) Observation andnot Always 1 0 Time andnot 0.00 Hash=78f011a0b5a0c65fa1cf106fcd62c845 [1] https://github.com/herd/herdtools7/pull/855 Signed-off-by: Puranjay Mohan Acked-by: Andrea Parri Signed-off-by: Paul E. McKenney Cc: Alan Stern Cc: Will Deacon Cc: Peter Zijlstra Cc: Boqun Feng Cc: Nicholas Piggin Cc: David Howells Cc: Jade Alglave Cc: Luc Maranget Cc: Akira Yokosawa Cc: Daniel Lustig Cc: Joel Fernandes Cc: --- tools/memory-model/linux-kernel.def | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'tools') diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def index d1f11930ec51..a12b96c547b7 100644 --- a/tools/memory-model/linux-kernel.def +++ b/tools/memory-model/linux-kernel.def @@ -70,6 +70,7 @@ atomic_or(V,X) { __atomic_op(X,|,V); } atomic_xor(V,X) { __atomic_op(X,^,V); } atomic_inc(X) { __atomic_op(X,+,1); } atomic_dec(X) { __atomic_op(X,-,1); } +atomic_andnot(V,X) { __atomic_op(X,&~,V); } atomic_add_return(V,X) __atomic_op_return{mb}(X,+,V) atomic_add_return_relaxed(V,X) __atomic_op_return{once}(X,+,V) @@ -138,3 +139,8 @@ atomic_add_negative(V,X) __atomic_op_return{mb}(X,+,V) < 0 atomic_add_negative_relaxed(V,X) __atomic_op_return{once}(X,+,V) < 0 atomic_add_negative_acquire(V,X) __atomic_op_return{acquire}(X,+,V) < 0 atomic_add_negative_release(V,X) __atomic_op_return{release}(X,+,V) < 0 + +atomic_fetch_andnot(V,X) __atomic_fetch_op{mb}(X,&~,V) +atomic_fetch_andnot_acquire(V,X) __atomic_fetch_op{acquire}(X,&~,V) +atomic_fetch_andnot_release(V,X) __atomic_fetch_op{release}(X,&~,V) +atomic_fetch_andnot_relaxed(V,X) __atomic_fetch_op{once}(X,&~,V) -- cgit v1.2.3 From de6f99723392f1c3a7bc103cba81bd9ba1d1708f Mon Sep 17 00:00:00 2001 From: Jonas Oberhauser Date: Mon, 30 Sep 2024 12:57:06 +0200 Subject: tools/memory-model: Legitimize current use of tags in LKMM macros 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/linux-kernel.bell | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'tools') diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell index ce068700939c..dba6b5b6dee0 100644 --- a/tools/memory-model/linux-kernel.bell +++ b/tools/memory-model/linux-kernel.bell @@ -16,10 +16,11 @@ enum Accesses = 'once (*READ_ONCE,WRITE_ONCE*) || 'release (*smp_store_release*) || 'acquire (*smp_load_acquire*) || - 'noreturn (* R of non-return RMW *) -instructions R[{'once,'acquire,'noreturn}] -instructions W[{'once,'release}] -instructions RMW[{'once,'acquire,'release}] + 'noreturn (* R of non-return RMW *) || + 'mb (*xchg(),cmpxchg(),...*) +instructions R[Accesses] +instructions W[Accesses] +instructions RMW[Accesses] enum Barriers = 'wmb (*smp_wmb*) || 'rmb (*smp_rmb*) || -- cgit v1.2.3 From 723177d712241238101b672b97b35734f86481f3 Mon Sep 17 00:00:00 2001 From: Jonas Oberhauser Date: Mon, 30 Sep 2024 12:57:07 +0200 Subject: tools/memory-model: Define applicable tags on operation in tools/... 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/linux-kernel.bell | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'tools') diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell index dba6b5b6dee0..7c9ae48b9437 100644 --- a/tools/memory-model/linux-kernel.bell +++ b/tools/memory-model/linux-kernel.bell @@ -36,6 +36,17 @@ enum Barriers = 'wmb (*smp_wmb*) || 'after-srcu-read-unlock (*smp_mb__after_srcu_read_unlock*) instructions F[Barriers] + +(* + * Filter out syntactic annotations that do not provide the corresponding + * semantic ordering, such as Acquire on a store or Mb on a failed RMW. + *) +let FailedRMW = RMW \ (domain(rmw) | range(rmw)) +let Acquire = Acquire \ W \ FailedRMW +let Release = Release \ R \ FailedRMW +let Mb = Mb \ FailedRMW +let Noreturn = Noreturn \ W + (* SRCU *) enum SRCU = 'srcu-lock || 'srcu-unlock || 'sync-srcu instructions SRCU[SRCU] -- cgit v1.2.3 From 29279349a566232057f52392d1a8af91772de7e1 Mon Sep 17 00:00:00 2001 From: Jonas Oberhauser Date: Mon, 30 Sep 2024 12:57:08 +0200 Subject: tools/memory-model: Define effect of Mb tags on RMWs in tools/... Herd7 transforms successful RMW with Mb tags by inserting smp_mb() fences around them. We emulate this by considering imaginary po-edges before the RMW read and before the RMW write, and extending the smp_mb() ordering rule, which currently only applies to real po edges that would be found around a really inserted smp_mb(), also to cases of the only imagined po edges. Reported-by: Viktor Vafeiadis Suggested-by: Alan Stern Signed-off-by: Jonas Oberhauser Signed-off-by: Paul E. McKenney Reviewed-by: Boqun Feng Tested-by: Boqun Feng --- tools/memory-model/linux-kernel.cat | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'tools') diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat index adf3c4f41229..d7e7bf13c831 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -34,6 +34,16 @@ let R4rmb = R \ Noreturn (* Reads for which rmb works *) let rmb = [R4rmb] ; fencerel(Rmb) ; [R4rmb] let wmb = [W] ; fencerel(Wmb) ; [W] let mb = ([M] ; fencerel(Mb) ; [M]) | + (* + * full-barrier RMWs (successful cmpxchg(), xchg(), etc.) act as + * though there were enclosed by smp_mb(). + * The effect of these virtual smp_mb() is formalized by adding + * Mb tags to the read and write of the operation, and providing + * the same ordering as though there were additional po edges + * between the Mb tag and the read resp. write. + *) + ([M] ; po ; [Mb & R]) | + ([Mb & W] ; po ; [M]) | ([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) | ([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) | ([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) | -- cgit v1.2.3 From fafa180683591f5f917bfa68e95aae463afc852a Mon Sep 17 00:00:00 2001 From: Jonas Oberhauser Date: Mon, 30 Sep 2024 12:57:09 +0200 Subject: tools/memory-model: Switch to softcoded herd7 tags 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 --- .../Documentation/herd-representation.txt | 27 ++++++++++++---------- tools/memory-model/README | 2 +- tools/memory-model/linux-kernel.bell | 3 +++ tools/memory-model/linux-kernel.cfg | 1 + tools/memory-model/linux-kernel.def | 18 ++++++++------- 5 files changed, 30 insertions(+), 21 deletions(-) (limited to 'tools') diff --git a/tools/memory-model/Documentation/herd-representation.txt b/tools/memory-model/Documentation/herd-representation.txt index ed988906f2b7..7ae1ff3d3769 100644 --- a/tools/memory-model/Documentation/herd-representation.txt +++ b/tools/memory-model/Documentation/herd-representation.txt @@ -18,6 +18,11 @@ # # By convention, a blank line in a cell means "same as the preceding line". # +# Note that the syntactic representation does not always match the sets and +# relations in linux-kernel.cat, due to redefinitions in linux-kernel.bell and +# lock.cat. For example, the po link between LKR and LKW is upgraded to an rmw +# link, and W[acquire] are not included in the Acquire set. +# # Disclaimer. The table includes representations of "add" and "and" operations; # corresponding/identical representations of "sub", "inc", "dec" and "or", "xor", # "andnot" operations are omitted. @@ -60,14 +65,13 @@ ------------------------------------------------------------------------------ | RMW ops w/o return value | | ------------------------------------------------------------------------------ - | atomic_add | R*[noreturn] ->rmw W*[once] | + | atomic_add | R*[noreturn] ->rmw W*[noreturn] | | 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_add_return | R*[mb] ->rmw W*[mb] | | atomic_fetch_add | | | atomic_fetch_and | | | atomic_xchg | | @@ -79,13 +83,13 @@ | atomic_xchg_relaxed | | | xchg_relaxed | | | atomic_add_negative_relaxed | | - | atomic_add_return_acquire | R*[acquire] ->rmw W*[once] | + | atomic_add_return_acquire | R*[acquire] ->rmw W*[acquire] | | 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_add_return_release | R*[release] ->rmw W*[release] | | atomic_fetch_add_release | | | atomic_fetch_and_release | | | atomic_xchg_release | | @@ -94,17 +98,16 @@ ------------------------------------------------------------------------------ | Conditional RMW ops | | ------------------------------------------------------------------------------ - | atomic_cmpxchg | On success: F[mb] ->po R*[once] | - | | ->rmw W*[once] ->po F[mb] | - | | On failure: R*[once] | + | atomic_cmpxchg | On success: R*[mb] ->rmw W*[mb] | + | | On failure: R*[mb] | | 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] | + | atomic_cmpxchg_acquire | On success: R*[acquire] ->rmw W*[acquire] | + | | On failure: R*[acquire] | + | atomic_cmpxchg_release | On success: R*[release] ->rmw W*[release] | + | | On failure: R*[release] | | spin_trylock | On success: LKR ->po LKW | | | On failure: LF | ------------------------------------------------------------------------------ diff --git a/tools/memory-model/README b/tools/memory-model/README index dab38904206a..59bc15edeb8a 100644 --- a/tools/memory-model/README +++ b/tools/memory-model/README @@ -20,7 +20,7 @@ that litmus test to be exercised within the Linux kernel. REQUIREMENTS ============ -Version 7.52 or higher of the "herd7" and "klitmus7" tools must be +Version 7.58 or higher of the "herd7" and "klitmus7" tools must be downloaded separately: https://github.com/herd/herdtools7 diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell index 7c9ae48b9437..8ae47545df97 100644 --- a/tools/memory-model/linux-kernel.bell +++ b/tools/memory-model/linux-kernel.bell @@ -94,3 +94,6 @@ let carry-dep = (data ; [~ Srcu-unlock] ; rfi)* let addr = carry-dep ; addr let ctrl = carry-dep ; ctrl let data = carry-dep ; data + +flag ~empty (if "lkmmv2" then 0 else _) + as this-model-requires-variant-higher-than-lkmmv1 diff --git a/tools/memory-model/linux-kernel.cfg b/tools/memory-model/linux-kernel.cfg index 3c8098e99f41..69b04f3aad73 100644 --- a/tools/memory-model/linux-kernel.cfg +++ b/tools/memory-model/linux-kernel.cfg @@ -1,6 +1,7 @@ macros linux-kernel.def bell linux-kernel.bell model linux-kernel.cat +variant lkmmv2 graph columns squished true showevents noregs diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def index a12b96c547b7..d7279a357cba 100644 --- a/tools/memory-model/linux-kernel.def +++ b/tools/memory-model/linux-kernel.def @@ -63,14 +63,14 @@ atomic_set(X,V) { WRITE_ONCE(*X,V); } atomic_read_acquire(X) smp_load_acquire(X) atomic_set_release(X,V) { smp_store_release(X,V); } -atomic_add(V,X) { __atomic_op(X,+,V); } -atomic_sub(V,X) { __atomic_op(X,-,V); } -atomic_and(V,X) { __atomic_op(X,&,V); } -atomic_or(V,X) { __atomic_op(X,|,V); } -atomic_xor(V,X) { __atomic_op(X,^,V); } -atomic_inc(X) { __atomic_op(X,+,1); } -atomic_dec(X) { __atomic_op(X,-,1); } -atomic_andnot(V,X) { __atomic_op(X,&~,V); } +atomic_add(V,X) { __atomic_op{noreturn}(X,+,V); } +atomic_sub(V,X) { __atomic_op{noreturn}(X,-,V); } +atomic_and(V,X) { __atomic_op{noreturn}(X,&,V); } +atomic_or(V,X) { __atomic_op{noreturn}(X,|,V); } +atomic_xor(V,X) { __atomic_op{noreturn}(X,^,V); } +atomic_inc(X) { __atomic_op{noreturn}(X,+,1); } +atomic_dec(X) { __atomic_op{noreturn}(X,-,1); } +atomic_andnot(V,X) { __atomic_op{noreturn}(X,&~,V); } atomic_add_return(V,X) __atomic_op_return{mb}(X,+,V) atomic_add_return_relaxed(V,X) __atomic_op_return{once}(X,+,V) @@ -144,3 +144,5 @@ atomic_fetch_andnot(V,X) __atomic_fetch_op{mb}(X,&~,V) atomic_fetch_andnot_acquire(V,X) __atomic_fetch_op{acquire}(X,&~,V) atomic_fetch_andnot_release(V,X) __atomic_fetch_op{release}(X,&~,V) atomic_fetch_andnot_relaxed(V,X) __atomic_fetch_op{once}(X,&~,V) + +atomic_add_unless(X,V,W) __atomic_add_unless{mb}(X,V,W) -- cgit v1.2.3 From dcc5197839f22655951056f399061872adfdb0b9 Mon Sep 17 00:00:00 2001 From: Jonas Oberhauser Date: Tue, 5 Nov 2024 17:48:58 +0100 Subject: tools/memory-model: Distinguish between syntactic and semantic tags 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 --- .../Documentation/herd-representation.txt | 44 ++--- tools/memory-model/linux-kernel.bell | 22 +-- tools/memory-model/linux-kernel.def | 198 ++++++++++----------- 3 files changed, 132 insertions(+), 132 deletions(-) (limited to 'tools') diff --git a/tools/memory-model/Documentation/herd-representation.txt b/tools/memory-model/Documentation/herd-representation.txt index 7ae1ff3d3769..4e19b4f2a476 100644 --- a/tools/memory-model/Documentation/herd-representation.txt +++ b/tools/memory-model/Documentation/herd-representation.txt @@ -21,7 +21,7 @@ # Note that the syntactic representation does not always match the sets and # relations in linux-kernel.cat, due to redefinitions in linux-kernel.bell and # lock.cat. For example, the po link between LKR and LKW is upgraded to an rmw -# link, and W[acquire] are not included in the Acquire set. +# link, and W[ACQUIRE] are not included in the Acquire set. # # Disclaimer. The table includes representations of "add" and "and" operations; # corresponding/identical representations of "sub", "inc", "dec" and "or", "xor", @@ -32,16 +32,16 @@ ------------------------------------------------------------------------------ | Non-RMW ops | | ------------------------------------------------------------------------------ - | READ_ONCE | R[once] | + | READ_ONCE | R[ONCE] | | atomic_read | | - | WRITE_ONCE | W[once] | + | WRITE_ONCE | W[ONCE] | | atomic_set | | - | smp_load_acquire | R[acquire] | + | smp_load_acquire | R[ACQUIRE] | | atomic_read_acquire | | - | smp_store_release | W[release] | + | smp_store_release | W[RELEASE] | | atomic_set_release | | - | smp_store_mb | W[once] ->po F[mb] | - | smp_mb | F[mb] | + | 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] | @@ -54,8 +54,8 @@ | 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] | + | rcu_dereference | R[ONCE] | + | rcu_assign_pointer | W[RELEASE] | | srcu_read_lock | R[srcu-lock] | | srcu_down_read | | | srcu_read_unlock | W[srcu-unlock] | @@ -65,31 +65,31 @@ ------------------------------------------------------------------------------ | RMW ops w/o return value | | ------------------------------------------------------------------------------ - | atomic_add | R*[noreturn] ->rmw W*[noreturn] | + | atomic_add | R*[NORETURN] ->rmw W*[NORETURN] | | atomic_and | | | spin_lock | LKR ->po LKW | ------------------------------------------------------------------------------ | RMW ops w/ return value | | ------------------------------------------------------------------------------ - | atomic_add_return | R*[mb] ->rmw W*[mb] | + | atomic_add_return | R*[MB] ->rmw W*[MB] | | atomic_fetch_add | | | atomic_fetch_and | | | atomic_xchg | | | xchg | | | atomic_add_negative | | - | atomic_add_return_relaxed | R*[once] ->rmw W*[once] | + | 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*[acquire] | + | atomic_add_return_acquire | R*[ACQUIRE] ->rmw W*[ACQUIRE] | | atomic_fetch_add_acquire | | | atomic_fetch_and_acquire | | | atomic_xchg_acquire | | | xchg_acquire | | | atomic_add_negative_acquire | | - | atomic_add_return_release | R*[release] ->rmw W*[release] | + | atomic_add_return_release | R*[RELEASE] ->rmw W*[RELEASE] | | atomic_fetch_add_release | | | atomic_fetch_and_release | | | atomic_xchg_release | | @@ -98,16 +98,16 @@ ------------------------------------------------------------------------------ | Conditional RMW ops | | ------------------------------------------------------------------------------ - | atomic_cmpxchg | On success: R*[mb] ->rmw W*[mb] | - | | On failure: R*[mb] | + | atomic_cmpxchg | On success: R*[MB] ->rmw W*[MB] | + | | On failure: R*[MB] | | 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*[acquire] | - | | On failure: R*[acquire] | - | atomic_cmpxchg_release | On success: R*[release] ->rmw W*[release] | - | | On failure: R*[release] | + | atomic_cmpxchg_relaxed | On success: R*[ONCE] ->rmw W*[ONCE] | + | | On failure: R*[ONCE] | + | atomic_cmpxchg_acquire | On success: R*[ACQUIRE] ->rmw W*[ACQUIRE] | + | | On failure: R*[ACQUIRE] | + | atomic_cmpxchg_release | On success: R*[RELEASE] ->rmw W*[RELEASE] | + | | On failure: R*[RELEASE] | | spin_trylock | On success: LKR ->po LKW | | | On failure: LF | ------------------------------------------------------------------------------ diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell index 8ae47545df97..fe65998002b9 100644 --- a/tools/memory-model/linux-kernel.bell +++ b/tools/memory-model/linux-kernel.bell @@ -13,18 +13,18 @@ "Linux-kernel memory consistency model" -enum Accesses = 'once (*READ_ONCE,WRITE_ONCE*) || - 'release (*smp_store_release*) || - 'acquire (*smp_load_acquire*) || - 'noreturn (* R of non-return RMW *) || - 'mb (*xchg(),cmpxchg(),...*) +enum Accesses = 'ONCE (*READ_ONCE,WRITE_ONCE*) || + 'RELEASE (*smp_store_release*) || + 'ACQUIRE (*smp_load_acquire*) || + 'NORETURN (* R of non-return RMW *) || + 'MB (*xchg(),cmpxchg(),...*) instructions R[Accesses] instructions W[Accesses] instructions RMW[Accesses] enum Barriers = 'wmb (*smp_wmb*) || 'rmb (*smp_rmb*) || - 'mb (*smp_mb*) || + 'MB (*smp_mb*) || 'barrier (*barrier*) || 'rcu-lock (*rcu_read_lock*) || 'rcu-unlock (*rcu_read_unlock*) || @@ -42,10 +42,10 @@ instructions F[Barriers] * semantic ordering, such as Acquire on a store or Mb on a failed RMW. *) let FailedRMW = RMW \ (domain(rmw) | range(rmw)) -let Acquire = Acquire \ W \ FailedRMW -let Release = Release \ R \ FailedRMW -let Mb = Mb \ FailedRMW -let Noreturn = Noreturn \ W +let Acquire = ACQUIRE \ W \ FailedRMW +let Release = RELEASE \ R \ FailedRMW +let Mb = MB \ FailedRMW +let Noreturn = NORETURN \ W (* SRCU *) enum SRCU = 'srcu-lock || 'srcu-unlock || 'sync-srcu @@ -85,7 +85,7 @@ flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep flag ~empty different-values(srcu-rscs) as srcu-bad-value-match (* Compute marked and plain memory accesses *) -let Marked = (~M) | IW | Once | Release | Acquire | domain(rmw) | range(rmw) | +let Marked = (~M) | IW | ONCE | RELEASE | ACQUIRE | MB | RMW | LKR | LKW | UL | LF | RL | RU | Srcu-lock | Srcu-unlock let Plain = M \ Marked diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def index d7279a357cba..49e402782e49 100644 --- a/tools/memory-model/linux-kernel.def +++ b/tools/memory-model/linux-kernel.def @@ -6,18 +6,18 @@ // which appeared in ASPLOS 2018. // ONCE -READ_ONCE(X) __load{once}(X) -WRITE_ONCE(X,V) { __store{once}(X,V); } +READ_ONCE(X) __load{ONCE}(X) +WRITE_ONCE(X,V) { __store{ONCE}(X,V); } // Release Acquire and friends -smp_store_release(X,V) { __store{release}(*X,V); } -smp_load_acquire(X) __load{acquire}(*X) -rcu_assign_pointer(X,V) { __store{release}(X,V); } -rcu_dereference(X) __load{once}(X) -smp_store_mb(X,V) { __store{once}(X,V); __fence{mb}; } +smp_store_release(X,V) { __store{RELEASE}(*X,V); } +smp_load_acquire(X) __load{ACQUIRE}(*X) +rcu_assign_pointer(X,V) { __store{RELEASE}(X,V); } +rcu_dereference(X) __load{ONCE}(X) +smp_store_mb(X,V) { __store{ONCE}(X,V); __fence{MB}; } // Fences -smp_mb() { __fence{mb}; } +smp_mb() { __fence{MB}; } smp_rmb() { __fence{rmb}; } smp_wmb() { __fence{wmb}; } smp_mb__before_atomic() { __fence{before-atomic}; } @@ -28,14 +28,14 @@ smp_mb__after_srcu_read_unlock() { __fence{after-srcu-read-unlock}; } barrier() { __fence{barrier}; } // Exchange -xchg(X,V) __xchg{mb}(X,V) -xchg_relaxed(X,V) __xchg{once}(X,V) -xchg_release(X,V) __xchg{release}(X,V) -xchg_acquire(X,V) __xchg{acquire}(X,V) -cmpxchg(X,V,W) __cmpxchg{mb}(X,V,W) -cmpxchg_relaxed(X,V,W) __cmpxchg{once}(X,V,W) -cmpxchg_acquire(X,V,W) __cmpxchg{acquire}(X,V,W) -cmpxchg_release(X,V,W) __cmpxchg{release}(X,V,W) +xchg(X,V) __xchg{MB}(X,V) +xchg_relaxed(X,V) __xchg{ONCE}(X,V) +xchg_release(X,V) __xchg{RELEASE}(X,V) +xchg_acquire(X,V) __xchg{ACQUIRE}(X,V) +cmpxchg(X,V,W) __cmpxchg{MB}(X,V,W) +cmpxchg_relaxed(X,V,W) __cmpxchg{ONCE}(X,V,W) +cmpxchg_acquire(X,V,W) __cmpxchg{ACQUIRE}(X,V,W) +cmpxchg_release(X,V,W) __cmpxchg{RELEASE}(X,V,W) // Spinlocks spin_lock(X) { __lock(X); } @@ -63,86 +63,86 @@ atomic_set(X,V) { WRITE_ONCE(*X,V); } atomic_read_acquire(X) smp_load_acquire(X) atomic_set_release(X,V) { smp_store_release(X,V); } -atomic_add(V,X) { __atomic_op{noreturn}(X,+,V); } -atomic_sub(V,X) { __atomic_op{noreturn}(X,-,V); } -atomic_and(V,X) { __atomic_op{noreturn}(X,&,V); } -atomic_or(V,X) { __atomic_op{noreturn}(X,|,V); } -atomic_xor(V,X) { __atomic_op{noreturn}(X,^,V); } -atomic_inc(X) { __atomic_op{noreturn}(X,+,1); } -atomic_dec(X) { __atomic_op{noreturn}(X,-,1); } -atomic_andnot(V,X) { __atomic_op{noreturn}(X,&~,V); } - -atomic_add_return(V,X) __atomic_op_return{mb}(X,+,V) -atomic_add_return_relaxed(V,X) __atomic_op_return{once}(X,+,V) -atomic_add_return_acquire(V,X) __atomic_op_return{acquire}(X,+,V) -atomic_add_return_release(V,X) __atomic_op_return{release}(X,+,V) -atomic_fetch_add(V,X) __atomic_fetch_op{mb}(X,+,V) -atomic_fetch_add_relaxed(V,X) __atomic_fetch_op{once}(X,+,V) -atomic_fetch_add_acquire(V,X) __atomic_fetch_op{acquire}(X,+,V) -atomic_fetch_add_release(V,X) __atomic_fetch_op{release}(X,+,V) - -atomic_fetch_and(V,X) __atomic_fetch_op{mb}(X,&,V) -atomic_fetch_and_relaxed(V,X) __atomic_fetch_op{once}(X,&,V) -atomic_fetch_and_acquire(V,X) __atomic_fetch_op{acquire}(X,&,V) -atomic_fetch_and_release(V,X) __atomic_fetch_op{release}(X,&,V) - -atomic_fetch_or(V,X) __atomic_fetch_op{mb}(X,|,V) -atomic_fetch_or_relaxed(V,X) __atomic_fetch_op{once}(X,|,V) -atomic_fetch_or_acquire(V,X) __atomic_fetch_op{acquire}(X,|,V) -atomic_fetch_or_release(V,X) __atomic_fetch_op{release}(X,|,V) - -atomic_fetch_xor(V,X) __atomic_fetch_op{mb}(X,^,V) -atomic_fetch_xor_relaxed(V,X) __atomic_fetch_op{once}(X,^,V) -atomic_fetch_xor_acquire(V,X) __atomic_fetch_op{acquire}(X,^,V) -atomic_fetch_xor_release(V,X) __atomic_fetch_op{release}(X,^,V) - -atomic_inc_return(X) __atomic_op_return{mb}(X,+,1) -atomic_inc_return_relaxed(X) __atomic_op_return{once}(X,+,1) -atomic_inc_return_acquire(X) __atomic_op_return{acquire}(X,+,1) -atomic_inc_return_release(X) __atomic_op_return{release}(X,+,1) -atomic_fetch_inc(X) __atomic_fetch_op{mb}(X,+,1) -atomic_fetch_inc_relaxed(X) __atomic_fetch_op{once}(X,+,1) -atomic_fetch_inc_acquire(X) __atomic_fetch_op{acquire}(X,+,1) -atomic_fetch_inc_release(X) __atomic_fetch_op{release}(X,+,1) - -atomic_sub_return(V,X) __atomic_op_return{mb}(X,-,V) -atomic_sub_return_relaxed(V,X) __atomic_op_return{once}(X,-,V) -atomic_sub_return_acquire(V,X) __atomic_op_return{acquire}(X,-,V) -atomic_sub_return_release(V,X) __atomic_op_return{release}(X,-,V) -atomic_fetch_sub(V,X) __atomic_fetch_op{mb}(X,-,V) -atomic_fetch_sub_relaxed(V,X) __atomic_fetch_op{once}(X,-,V) -atomic_fetch_sub_acquire(V,X) __atomic_fetch_op{acquire}(X,-,V) -atomic_fetch_sub_release(V,X) __atomic_fetch_op{release}(X,-,V) - -atomic_dec_return(X) __atomic_op_return{mb}(X,-,1) -atomic_dec_return_relaxed(X) __atomic_op_return{once}(X,-,1) -atomic_dec_return_acquire(X) __atomic_op_return{acquire}(X,-,1) -atomic_dec_return_release(X) __atomic_op_return{release}(X,-,1) -atomic_fetch_dec(X) __atomic_fetch_op{mb}(X,-,1) -atomic_fetch_dec_relaxed(X) __atomic_fetch_op{once}(X,-,1) -atomic_fetch_dec_acquire(X) __atomic_fetch_op{acquire}(X,-,1) -atomic_fetch_dec_release(X) __atomic_fetch_op{release}(X,-,1) - -atomic_xchg(X,V) __xchg{mb}(X,V) -atomic_xchg_relaxed(X,V) __xchg{once}(X,V) -atomic_xchg_release(X,V) __xchg{release}(X,V) -atomic_xchg_acquire(X,V) __xchg{acquire}(X,V) -atomic_cmpxchg(X,V,W) __cmpxchg{mb}(X,V,W) -atomic_cmpxchg_relaxed(X,V,W) __cmpxchg{once}(X,V,W) -atomic_cmpxchg_acquire(X,V,W) __cmpxchg{acquire}(X,V,W) -atomic_cmpxchg_release(X,V,W) __cmpxchg{release}(X,V,W) - -atomic_sub_and_test(V,X) __atomic_op_return{mb}(X,-,V) == 0 -atomic_dec_and_test(X) __atomic_op_return{mb}(X,-,1) == 0 -atomic_inc_and_test(X) __atomic_op_return{mb}(X,+,1) == 0 -atomic_add_negative(V,X) __atomic_op_return{mb}(X,+,V) < 0 -atomic_add_negative_relaxed(V,X) __atomic_op_return{once}(X,+,V) < 0 -atomic_add_negative_acquire(V,X) __atomic_op_return{acquire}(X,+,V) < 0 -atomic_add_negative_release(V,X) __atomic_op_return{release}(X,+,V) < 0 - -atomic_fetch_andnot(V,X) __atomic_fetch_op{mb}(X,&~,V) -atomic_fetch_andnot_acquire(V,X) __atomic_fetch_op{acquire}(X,&~,V) -atomic_fetch_andnot_release(V,X) __atomic_fetch_op{release}(X,&~,V) -atomic_fetch_andnot_relaxed(V,X) __atomic_fetch_op{once}(X,&~,V) - -atomic_add_unless(X,V,W) __atomic_add_unless{mb}(X,V,W) +atomic_add(V,X) { __atomic_op{NORETURN}(X,+,V); } +atomic_sub(V,X) { __atomic_op{NORETURN}(X,-,V); } +atomic_and(V,X) { __atomic_op{NORETURN}(X,&,V); } +atomic_or(V,X) { __atomic_op{NORETURN}(X,|,V); } +atomic_xor(V,X) { __atomic_op{NORETURN}(X,^,V); } +atomic_inc(X) { __atomic_op{NORETURN}(X,+,1); } +atomic_dec(X) { __atomic_op{NORETURN}(X,-,1); } +atomic_andnot(V,X) { __atomic_op{NORETURN}(X,&~,V); } + +atomic_add_return(V,X) __atomic_op_return{MB}(X,+,V) +atomic_add_return_relaxed(V,X) __atomic_op_return{ONCE}(X,+,V) +atomic_add_return_acquire(V,X) __atomic_op_return{ACQUIRE}(X,+,V) +atomic_add_return_release(V,X) __atomic_op_return{RELEASE}(X,+,V) +atomic_fetch_add(V,X) __atomic_fetch_op{MB}(X,+,V) +atomic_fetch_add_relaxed(V,X) __atomic_fetch_op{ONCE}(X,+,V) +atomic_fetch_add_acquire(V,X) __atomic_fetch_op{ACQUIRE}(X,+,V) +atomic_fetch_add_release(V,X) __atomic_fetch_op{RELEASE}(X,+,V) + +atomic_fetch_and(V,X) __atomic_fetch_op{MB}(X,&,V) +atomic_fetch_and_relaxed(V,X) __atomic_fetch_op{ONCE}(X,&,V) +atomic_fetch_and_acquire(V,X) __atomic_fetch_op{ACQUIRE}(X,&,V) +atomic_fetch_and_release(V,X) __atomic_fetch_op{RELEASE}(X,&,V) + +atomic_fetch_or(V,X) __atomic_fetch_op{MB}(X,|,V) +atomic_fetch_or_relaxed(V,X) __atomic_fetch_op{ONCE}(X,|,V) +atomic_fetch_or_acquire(V,X) __atomic_fetch_op{ACQUIRE}(X,|,V) +atomic_fetch_or_release(V,X) __atomic_fetch_op{RELEASE}(X,|,V) + +atomic_fetch_xor(V,X) __atomic_fetch_op{MB}(X,^,V) +atomic_fetch_xor_relaxed(V,X) __atomic_fetch_op{ONCE}(X,^,V) +atomic_fetch_xor_acquire(V,X) __atomic_fetch_op{ACQUIRE}(X,^,V) +atomic_fetch_xor_release(V,X) __atomic_fetch_op{RELEASE}(X,^,V) + +atomic_inc_return(X) __atomic_op_return{MB}(X,+,1) +atomic_inc_return_relaxed(X) __atomic_op_return{ONCE}(X,+,1) +atomic_inc_return_acquire(X) __atomic_op_return{ACQUIRE}(X,+,1) +atomic_inc_return_release(X) __atomic_op_return{RELEASE}(X,+,1) +atomic_fetch_inc(X) __atomic_fetch_op{MB}(X,+,1) +atomic_fetch_inc_relaxed(X) __atomic_fetch_op{ONCE}(X,+,1) +atomic_fetch_inc_acquire(X) __atomic_fetch_op{ACQUIRE}(X,+,1) +atomic_fetch_inc_release(X) __atomic_fetch_op{RELEASE}(X,+,1) + +atomic_sub_return(V,X) __atomic_op_return{MB}(X,-,V) +atomic_sub_return_relaxed(V,X) __atomic_op_return{ONCE}(X,-,V) +atomic_sub_return_acquire(V,X) __atomic_op_return{ACQUIRE}(X,-,V) +atomic_sub_return_release(V,X) __atomic_op_return{RELEASE}(X,-,V) +atomic_fetch_sub(V,X) __atomic_fetch_op{MB}(X,-,V) +atomic_fetch_sub_relaxed(V,X) __atomic_fetch_op{ONCE}(X,-,V) +atomic_fetch_sub_acquire(V,X) __atomic_fetch_op{ACQUIRE}(X,-,V) +atomic_fetch_sub_release(V,X) __atomic_fetch_op{RELEASE}(X,-,V) + +atomic_dec_return(X) __atomic_op_return{MB}(X,-,1) +atomic_dec_return_relaxed(X) __atomic_op_return{ONCE}(X,-,1) +atomic_dec_return_acquire(X) __atomic_op_return{ACQUIRE}(X,-,1) +atomic_dec_return_release(X) __atomic_op_return{RELEASE}(X,-,1) +atomic_fetch_dec(X) __atomic_fetch_op{MB}(X,-,1) +atomic_fetch_dec_relaxed(X) __atomic_fetch_op{ONCE}(X,-,1) +atomic_fetch_dec_acquire(X) __atomic_fetch_op{ACQUIRE}(X,-,1) +atomic_fetch_dec_release(X) __atomic_fetch_op{RELEASE}(X,-,1) + +atomic_xchg(X,V) __xchg{MB}(X,V) +atomic_xchg_relaxed(X,V) __xchg{ONCE}(X,V) +atomic_xchg_release(X,V) __xchg{RELEASE}(X,V) +atomic_xchg_acquire(X,V) __xchg{ACQUIRE}(X,V) +atomic_cmpxchg(X,V,W) __cmpxchg{MB}(X,V,W) +atomic_cmpxchg_relaxed(X,V,W) __cmpxchg{ONCE}(X,V,W) +atomic_cmpxchg_acquire(X,V,W) __cmpxchg{ACQUIRE}(X,V,W) +atomic_cmpxchg_release(X,V,W) __cmpxchg{RELEASE}(X,V,W) + +atomic_sub_and_test(V,X) __atomic_op_return{MB}(X,-,V) == 0 +atomic_dec_and_test(X) __atomic_op_return{MB}(X,-,1) == 0 +atomic_inc_and_test(X) __atomic_op_return{MB}(X,+,1) == 0 +atomic_add_negative(V,X) __atomic_op_return{MB}(X,+,V) < 0 +atomic_add_negative_relaxed(V,X) __atomic_op_return{ONCE}(X,+,V) < 0 +atomic_add_negative_acquire(V,X) __atomic_op_return{ACQUIRE}(X,+,V) < 0 +atomic_add_negative_release(V,X) __atomic_op_return{RELEASE}(X,+,V) < 0 + +atomic_fetch_andnot(V,X) __atomic_fetch_op{MB}(X,&~,V) +atomic_fetch_andnot_acquire(V,X) __atomic_fetch_op{ACQUIRE}(X,&~,V) +atomic_fetch_andnot_release(V,X) __atomic_fetch_op{RELEASE}(X,&~,V) +atomic_fetch_andnot_relaxed(V,X) __atomic_fetch_op{ONCE}(X,&~,V) + +atomic_add_unless(X,V,W) __atomic_add_unless{MB}(X,V,W) -- cgit v1.2.3 From fa9e35a0772a74fc190265a5d4e3e62384b999ff Mon Sep 17 00:00:00 2001 From: Akira Yokosawa Date: Tue, 25 Feb 2025 18:39:58 +0900 Subject: tools/memory-model/README: Fix typo Fix a trivial typo. Signed-off-by: Akira Yokosawa Signed-off-by: Paul E. McKenney --- tools/memory-model/README | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tools') diff --git a/tools/memory-model/README b/tools/memory-model/README index 59bc15edeb8a..64c860863aa9 100644 --- a/tools/memory-model/README +++ b/tools/memory-model/README @@ -79,7 +79,7 @@ Several thousand more example litmus tests are available here: https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/herd https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/litmus -Documentation describing litmus tests and now to use them may be found +Documentation describing litmus tests and how to use them may be found here: tools/memory-model/Documentation/litmus-tests.txt -- cgit v1.2.3 From a2bfbf847c96196d62c9a59bd32e1fdafd1c205c Mon Sep 17 00:00:00 2001 From: Akira Yokosawa Date: Tue, 25 Feb 2025 18:41:48 +0900 Subject: tools/memory-model: glossary.txt: Fix indents There are a couple of inconsistent indents around code/literal blocks. Adjust them to make this file easier to parse. Signed-off-by: Akira Yokosawa Signed-off-by: Paul E. McKenney --- tools/memory-model/Documentation/glossary.txt | 32 +++++++++++++-------------- 1 file changed, 16 insertions(+), 16 deletions(-) (limited to 'tools') diff --git a/tools/memory-model/Documentation/glossary.txt b/tools/memory-model/Documentation/glossary.txt index 6f3d16dbf467..7ead94bffa4e 100644 --- a/tools/memory-model/Documentation/glossary.txt +++ b/tools/memory-model/Documentation/glossary.txt @@ -15,14 +15,14 @@ Address Dependency: When the address of a later memory access is computed 3 do_something(p->a); 4 rcu_read_unlock(); - In this case, because the address of "p->a" on line 3 is computed - from the value returned by the rcu_dereference() on line 2, the - address dependency extends from that rcu_dereference() to that - "p->a". In rare cases, optimizing compilers can destroy address - dependencies. Please see Documentation/RCU/rcu_dereference.rst - for more information. + In this case, because the address of "p->a" on line 3 is computed + from the value returned by the rcu_dereference() on line 2, the + address dependency extends from that rcu_dereference() to that + "p->a". In rare cases, optimizing compilers can destroy address + dependencies. Please see Documentation/RCU/rcu_dereference.rst + for more information. - See also "Control Dependency" and "Data Dependency". + See also "Control Dependency" and "Data Dependency". Acquire: With respect to a lock, acquiring that lock, for example, using spin_lock(). With respect to a non-lock shared variable, @@ -59,12 +59,12 @@ Control Dependency: When a later store's execution depends on a test 1 if (READ_ONCE(x)) 2 WRITE_ONCE(y, 1); - Here, the control dependency extends from the READ_ONCE() on - line 1 to the WRITE_ONCE() on line 2. Control dependencies are - fragile, and can be easily destroyed by optimizing compilers. - Please see control-dependencies.txt for more information. + Here, the control dependency extends from the READ_ONCE() on + line 1 to the WRITE_ONCE() on line 2. Control dependencies are + fragile, and can be easily destroyed by optimizing compilers. + Please see control-dependencies.txt for more information. - See also "Address Dependency" and "Data Dependency". + See also "Address Dependency" and "Data Dependency". Cycle: Memory-barrier pairing is restricted to a pair of CPUs, as the name suggests. And in a great many cases, a pair of CPUs is all @@ -72,10 +72,10 @@ Cycle: Memory-barrier pairing is restricted to a pair of CPUs, as the extended to additional CPUs, and the result is called a "cycle". In a cycle, each CPU's ordering interacts with that of the next: - CPU 0 CPU 1 CPU 2 - WRITE_ONCE(x, 1); WRITE_ONCE(y, 1); WRITE_ONCE(z, 1); - smp_mb(); smp_mb(); smp_mb(); - r0 = READ_ONCE(y); r1 = READ_ONCE(z); r2 = READ_ONCE(x); + CPU 0 CPU 1 CPU 2 + WRITE_ONCE(x, 1); WRITE_ONCE(y, 1); WRITE_ONCE(z, 1); + smp_mb(); smp_mb(); smp_mb(); + r0 = READ_ONCE(y); r1 = READ_ONCE(z); r2 = READ_ONCE(x); CPU 0's smp_mb() interacts with that of CPU 1, which interacts with that of CPU 2, which in turn interacts with that of CPU 0 -- cgit v1.2.3