* [PATCH v3 0/5] tools/memory-model: Define more of LKMM in tools/memory-model
@ 2024-09-19 13:06 Jonas Oberhauser
2024-09-19 13:06 ` [PATCH v3 1/5] tools/memory-model: Legitimize current use of tags in LKMM macros Jonas Oberhauser
` (4 more replies)
0 siblings, 5 replies; 10+ messages in thread
From: Jonas Oberhauser @ 2024-09-19 13:06 UTC (permalink / raw)
To: paulmck
Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells,
j.alglave, luc.maranget, akiyks, dlustig, joel, urezki,
quic_neeraju, frederic, linux-kernel, lkmm, hernan.poncedeleon,
Jonas Oberhauser
Currently, the effect of several tag on operations is defined only in
the herd7 tool's OCaml code as syntax transformations, while the effect
of all other tags is defined in tools/memory-model.
This asymmetry means that two seemingly analogous definitions in
tools/memory-model behave quite differently because the generated
representation is sometimes modified by hardcoded behavior in herd7.
It also makes it hard to see that the behavior of the formalization
matches the intuition described in explanation.txt without delving into
the implementation of herd7.
Furthermore, this hardcoded behavior is hard to maintain inside herd7 and
other tools implementing WMM, and has caused several bugs and confusions
with the tool maintainers, e.g.:
https://github.com/MPI-SWS/genmc/issues/22
https://github.com/herd/herdtools7/issues/384#issuecomment-1132859904
https://github.com/hernanponcedeleon/Dat3M/issues/254
It also means that potential future extensions of LKMM with new tags may
not work without changing internals of the herd7 tool.
In this patch series, we first emulate the effect of herd7 transformations
in tools/memory-model through explicit rules in .cat and .bell files that
reference the transformed tags.
These transformations do not have any immediate effect with the current
herd7 implementation, because they apply after the syntax transformations
have already modified those tags.
In a second step, we then distinguish between syntactic tags (that are
placed by the programmer on operations, e.g., an 'ACQUIRE tag on both the
read and write of an xchg_acquire() operation) and sets of events (that
would be defined after the (emulated) transformations, e.g., an Acquire
set that includes only on the read of the xchg_acquire(), but "has been
removed" from the write).
This second step (comprising patches 4 and 5) is incompatible with the
current herd7 implementation, since herd7 uses hardcoded tag names to decide
what to do with LKMM; therefore, the newly introduced syntactic tags will be
ignored or processed incorrectly by herd7.
Have fun,
jonas
Changes from v1 to v2:
- addressed several spelling/style issues pointed out by Alan
- simplified the definition of Marked accesses based on a
suggestion by Alan
Changes from v2 to v3:
- addressed imprecise comment pointed out by Boqun
- addressed the backwards compatibility issue pointed out by Akira
with help of Hernan: improved version compatibility by adding
an error message on older versions of herd and relying on a new
flag -lkmmv1 to select the version
- integrated recent patches, like the herd representation table
and primitives like atomic_add_unless or atomic_and_not
Jonas Oberhauser (5):
tools/memory-model: Legitimize current use of tags in LKMM macros
tools/memory-model: Define applicable tags on operation in tools/...
tools/memory-model: Define effect of Mb tags on RMWs in tools/...
tools/memory-model: Switch to softcoded herd7 tags
tools/memory-model: Distinguish between syntactic and semantic tags
.../Documentation/herd-representation.txt | 27 +--
tools/memory-model/linux-kernel.bell | 33 ++-
tools/memory-model/linux-kernel.cat | 10 +
tools/memory-model/linux-kernel.cfg | 1 +
tools/memory-model/linux-kernel.def | 196 +++++++++---------
.../litmus-tests/add-unless-mb.litmus | 27 +++
6 files changed, 176 insertions(+), 118 deletions(-)
create mode 100644 tools/memory-model/litmus-tests/add-unless-mb.litmus
--
2.34.1
^ permalink raw reply [flat|nested] 10+ messages in thread* [PATCH v3 1/5] tools/memory-model: Legitimize current use of tags in LKMM macros 2024-09-19 13:06 [PATCH v3 0/5] tools/memory-model: Define more of LKMM in tools/memory-model Jonas Oberhauser @ 2024-09-19 13:06 ` Jonas Oberhauser 2024-09-19 13:06 ` [PATCH v3 2/5] tools/memory-model: Define applicable tags on operation in tools/ Jonas Oberhauser ` (3 subsequent siblings) 4 siblings, 0 replies; 10+ messages in thread From: Jonas Oberhauser @ 2024-09-19 13:06 UTC (permalink / raw) To: paulmck Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget, akiyks, dlustig, joel, urezki, quic_neeraju, frederic, linux-kernel, lkmm, hernan.poncedeleon, Jonas Oberhauser 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 <jonas.oberhauser@huaweicloud.com> --- tools/memory-model/linux-kernel.bell | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) 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*) || -- 2.34.1 ^ permalink raw reply [flat|nested] 10+ messages in thread
* [PATCH v3 2/5] tools/memory-model: Define applicable tags on operation in tools/... 2024-09-19 13:06 [PATCH v3 0/5] tools/memory-model: Define more of LKMM in tools/memory-model Jonas Oberhauser 2024-09-19 13:06 ` [PATCH v3 1/5] tools/memory-model: Legitimize current use of tags in LKMM macros Jonas Oberhauser @ 2024-09-19 13:06 ` Jonas Oberhauser 2024-09-19 13:06 ` [PATCH v3 3/5] tools/memory-model: Define effect of Mb tags on RMWs " Jonas Oberhauser ` (2 subsequent siblings) 4 siblings, 0 replies; 10+ messages in thread From: Jonas Oberhauser @ 2024-09-19 13:06 UTC (permalink / raw) To: paulmck Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget, akiyks, dlustig, joel, urezki, quic_neeraju, frederic, linux-kernel, lkmm, hernan.poncedeleon, Jonas Oberhauser 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 <jonas.oberhauser@huaweicloud.com> --- tools/memory-model/linux-kernel.bell | 11 +++++++++++ 1 file changed, 11 insertions(+) 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] -- 2.34.1 ^ permalink raw reply [flat|nested] 10+ messages in thread
* [PATCH v3 3/5] tools/memory-model: Define effect of Mb tags on RMWs in tools/... 2024-09-19 13:06 [PATCH v3 0/5] tools/memory-model: Define more of LKMM in tools/memory-model Jonas Oberhauser 2024-09-19 13:06 ` [PATCH v3 1/5] tools/memory-model: Legitimize current use of tags in LKMM macros Jonas Oberhauser 2024-09-19 13:06 ` [PATCH v3 2/5] tools/memory-model: Define applicable tags on operation in tools/ Jonas Oberhauser @ 2024-09-19 13:06 ` Jonas Oberhauser 2024-09-19 13:06 ` [PATCH v3 4/5] tools/memory-model: Switch to softcoded herd7 tags Jonas Oberhauser 2024-09-19 13:06 ` [PATCH v3 5/5] tools/memory-model: Distinguish between syntactic and semantic tags Jonas Oberhauser 4 siblings, 0 replies; 10+ messages in thread From: Jonas Oberhauser @ 2024-09-19 13:06 UTC (permalink / raw) To: paulmck Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget, akiyks, dlustig, joel, urezki, quic_neeraju, frederic, linux-kernel, lkmm, hernan.poncedeleon, Jonas Oberhauser, Viktor Vafeiadis 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 <viktor@mpi-sws.org> Suggested-by: Alan Stern <stern@rowland.harvard.edu> Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com> --- tools/memory-model/linux-kernel.cat | 10 ++++++++++ 1 file changed, 10 insertions(+) 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]) | -- 2.34.1 ^ permalink raw reply [flat|nested] 10+ messages in thread
* [PATCH v3 4/5] tools/memory-model: Switch to softcoded herd7 tags 2024-09-19 13:06 [PATCH v3 0/5] tools/memory-model: Define more of LKMM in tools/memory-model Jonas Oberhauser ` (2 preceding siblings ...) 2024-09-19 13:06 ` [PATCH v3 3/5] tools/memory-model: Define effect of Mb tags on RMWs " Jonas Oberhauser @ 2024-09-19 13:06 ` Jonas Oberhauser 2024-09-20 12:23 ` Hernan Ponce de Leon 2024-09-21 2:44 ` Akira Yokosawa 2024-09-19 13:06 ` [PATCH v3 5/5] tools/memory-model: Distinguish between syntactic and semantic tags Jonas Oberhauser 4 siblings, 2 replies; 10+ messages in thread From: Jonas Oberhauser @ 2024-09-19 13:06 UTC (permalink / raw) To: paulmck Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget, akiyks, dlustig, joel, urezki, quic_neeraju, frederic, linux-kernel, lkmm, hernan.poncedeleon, Jonas Oberhauser A new version of Herd7 provides a -lkmmv1 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. We also add a litmus test for atomic_add_unless which uncovered a bug in early iterations of the Herd7 patch that implements the new switch. (To be) Signed-off-by: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com> Signed-off by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com> --- .../Documentation/herd-representation.txt | 27 ++++++++++--------- tools/memory-model/linux-kernel.bell | 3 +++ tools/memory-model/linux-kernel.cfg | 1 + tools/memory-model/linux-kernel.def | 18 +++++++------ .../litmus-tests/add-unless-mb.litmus | 27 +++++++++++++++++++ 5 files changed, 56 insertions(+), 20 deletions(-) create mode 100644 tools/memory-model/litmus-tests/add-unless-mb.litmus 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/linux-kernel.bell b/tools/memory-model/linux-kernel.bell index 7c9ae48b9437..703028e5e091 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 "lkmmv1" then 0 else _) + as this-model-requires-variant-higher-than-lkmmv0 diff --git a/tools/memory-model/linux-kernel.cfg b/tools/memory-model/linux-kernel.cfg index 3c8098e99f41..a5855363259a 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 lkmmv1 graph columns squished true showevents noregs diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def index a12b96c547b7..4281572732bd 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) \ No newline at end of file diff --git a/tools/memory-model/litmus-tests/add-unless-mb.litmus b/tools/memory-model/litmus-tests/add-unless-mb.litmus new file mode 100644 index 000000000000..72f76ff3f59d --- /dev/null +++ b/tools/memory-model/litmus-tests/add-unless-mb.litmus @@ -0,0 +1,27 @@ +C add_unless_mb + +(* + * Result: Never + * + * This litmus test demonstrates that a successful atomic_add_unless + * acts as a full memory barrier, ensuring that *x=1 propagates to P1 + * before P1 executes *x=2. + *) + +{} + +P0(atomic_t *x, atomic_t *y, atomic_t *z) +{ + WRITE_ONCE(*x, 1); + int r0 = atomic_add_unless(z,1,5); + WRITE_ONCE(*y, 1); +} + +P1(atomic_t *x, atomic_t *y) +{ + int r0 = READ_ONCE(*y); + if (r0 == 1) + WRITE_ONCE(*x, 2); +} + +exists (1:r0=1 /\ x=1) -- 2.34.1 ^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: [PATCH v3 4/5] tools/memory-model: Switch to softcoded herd7 tags 2024-09-19 13:06 ` [PATCH v3 4/5] tools/memory-model: Switch to softcoded herd7 tags Jonas Oberhauser @ 2024-09-20 12:23 ` Hernan Ponce de Leon 2024-09-21 2:44 ` Akira Yokosawa 1 sibling, 0 replies; 10+ messages in thread From: Hernan Ponce de Leon @ 2024-09-20 12:23 UTC (permalink / raw) To: Jonas Oberhauser, paulmck Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget, akiyks, dlustig, joel, urezki, quic_neeraju, frederic, linux-kernel, lkmm On 9/19/2024 3:06 PM, Jonas Oberhauser wrote: > A new version of Herd7 provides a -lkmmv1 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. The changes to herd7 are ready to be merged. https://github.com/herd/herdtools7/pull/865 I just asked Luc to put this on hold until this series is reviewed to be sure no more changes are needed. > > 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. > > We also add a litmus test for atomic_add_unless which uncovered a bug in early > iterations of the Herd7 patch that implements the new switch. > > (To be) Signed-off-by: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com> Signed-off-by: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com> > Signed-off by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com> > --- > .../Documentation/herd-representation.txt | 27 ++++++++++--------- > tools/memory-model/linux-kernel.bell | 3 +++ > tools/memory-model/linux-kernel.cfg | 1 + > tools/memory-model/linux-kernel.def | 18 +++++++------ > .../litmus-tests/add-unless-mb.litmus | 27 +++++++++++++++++++ > 5 files changed, 56 insertions(+), 20 deletions(-) > create mode 100644 tools/memory-model/litmus-tests/add-unless-mb.litmus > > 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/linux-kernel.bell b/tools/memory-model/linux-kernel.bell > index 7c9ae48b9437..703028e5e091 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 "lkmmv1" then 0 else _) > + as this-model-requires-variant-higher-than-lkmmv0 > diff --git a/tools/memory-model/linux-kernel.cfg b/tools/memory-model/linux-kernel.cfg > index 3c8098e99f41..a5855363259a 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 lkmmv1 > graph columns > squished true > showevents noregs > diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def > index a12b96c547b7..4281572732bd 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) > \ No newline at end of file > diff --git a/tools/memory-model/litmus-tests/add-unless-mb.litmus b/tools/memory-model/litmus-tests/add-unless-mb.litmus > new file mode 100644 > index 000000000000..72f76ff3f59d > --- /dev/null > +++ b/tools/memory-model/litmus-tests/add-unless-mb.litmus > @@ -0,0 +1,27 @@ > +C add_unless_mb > + > +(* > + * Result: Never > + * > + * This litmus test demonstrates that a successful atomic_add_unless > + * acts as a full memory barrier, ensuring that *x=1 propagates to P1 > + * before P1 executes *x=2. > + *) > + > +{} > + > +P0(atomic_t *x, atomic_t *y, atomic_t *z) > +{ > + WRITE_ONCE(*x, 1); > + int r0 = atomic_add_unless(z,1,5); > + WRITE_ONCE(*y, 1); > +} > + > +P1(atomic_t *x, atomic_t *y) > +{ > + int r0 = READ_ONCE(*y); > + if (r0 == 1) > + WRITE_ONCE(*x, 2); > +} > + > +exists (1:r0=1 /\ x=1) ^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: [PATCH v3 4/5] tools/memory-model: Switch to softcoded herd7 tags 2024-09-19 13:06 ` [PATCH v3 4/5] tools/memory-model: Switch to softcoded herd7 tags Jonas Oberhauser 2024-09-20 12:23 ` Hernan Ponce de Leon @ 2024-09-21 2:44 ` Akira Yokosawa 2024-09-21 7:39 ` Jonas Oberhauser 1 sibling, 1 reply; 10+ messages in thread From: Akira Yokosawa @ 2024-09-21 2:44 UTC (permalink / raw) To: Jonas Oberhauser, paulmck Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget, dlustig, joel, urezki, quic_neeraju, frederic, linux-kernel, lkmm, hernan.poncedeleon, Akira Yokosawa On Thu, 19 Sep 2024 15:06:33 +0200, Jonas Oberhauser wrote: > A new version of Herd7 provides a -lkmmv1 switch which overrides the old herd7 Why -lkmmv1? You mean current (unversioned) LKMM has to be called v0 ??? My preference is to call current one as v1 and your new version as v2. Either way, Reviewed-by: Akira Yokosawa <akiyks@gmail.com> Please find a few more comments inline below. > 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. > > We also add a litmus test for atomic_add_unless which uncovered a bug in early > iterations of the Herd7 patch that implements the new switch. > > (To be) Signed-off-by: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com> > Signed-off by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com> > --- > .../Documentation/herd-representation.txt | 27 ++++++++++--------- > tools/memory-model/linux-kernel.bell | 3 +++ > tools/memory-model/linux-kernel.cfg | 1 + > tools/memory-model/linux-kernel.def | 18 +++++++------ > .../litmus-tests/add-unless-mb.litmus | 27 +++++++++++++++++++ > 5 files changed, 56 insertions(+), 20 deletions(-) > create mode 100644 tools/memory-model/litmus-tests/add-unless-mb.litmus > [...] > diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def > index a12b96c547b7..4281572732bd 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) > \ No newline at end of file Please fix this warning. > diff --git a/tools/memory-model/litmus-tests/add-unless-mb.litmus b/tools/memory-model/litmus-tests/add-unless-mb.litmus > new file mode 100644 > index 000000000000..72f76ff3f59d > --- /dev/null > +++ b/tools/memory-model/litmus-tests/add-unless-mb.litmus > @@ -0,0 +1,27 @@ > +C add_unless_mb > + > +(* > + * Result: Never > + * > + * This litmus test demonstrates that a successful atomic_add_unless > + * acts as a full memory barrier, ensuring that *x=1 propagates to P1 > + * before P1 executes *x=2. > + *) > + > +{} > + > +P0(atomic_t *x, atomic_t *y, atomic_t *z) > +{ > + WRITE_ONCE(*x, 1); > + int r0 = atomic_add_unless(z,1,5); > + WRITE_ONCE(*y, 1); > +} > + > +P1(atomic_t *x, atomic_t *y) > +{ > + int r0 = READ_ONCE(*y); > + if (r0 == 1) > + WRITE_ONCE(*x, 2); > +} > + > +exists (1:r0=1 /\ x=1) This litmus test is not compatible with klitmus7, which is much stricter than herd7's C parser. You can have only int or int* variables in the exists clause. Register variables need their declarations at the top of each Pn() (classic C). See below for klitmus7 ready code. And tools/memory-model/litmus-tests/README need to mention this litmus test. Thanks, Akira --------------------------------------------- P0(int *x, int *y, atomic_t *z) { int r0; WRITE_ONCE(*x, 1); r0 = atomic_add_unless(z,1,5); WRITE_ONCE(*y, 1); } P1(int *x, int *y) { int r0; r0 = READ_ONCE(*y); if (r0 == 1) WRITE_ONCE(*x, 2); } exists (1:r0=1 /\ x=1) --------------------------------------------- ^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: [PATCH v3 4/5] tools/memory-model: Switch to softcoded herd7 tags 2024-09-21 2:44 ` Akira Yokosawa @ 2024-09-21 7:39 ` Jonas Oberhauser 2024-09-21 11:28 ` Akira Yokosawa 0 siblings, 1 reply; 10+ messages in thread From: Jonas Oberhauser @ 2024-09-21 7:39 UTC (permalink / raw) To: Akira Yokosawa, paulmck Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget, dlustig, joel, urezki, quic_neeraju, frederic, linux-kernel, lkmm, hernan.poncedeleon Thanks Akira for your continued eagle eyes! Will include in next revision. One question below. jonas Am 9/21/2024 um 4:44 AM schrieb Akira Yokosawa: > This litmus test is not compatible with klitmus7, which is much > stricter than herd7's C parser. > > You can have only int or int* variables in the exists clause. > Register variables need their declarations at the top of each Pn() > (classic C). > > See below for klitmus7 ready code. > > And tools/memory-model/litmus-tests/README need to mention this > litmus test. > > Thanks, Akira > > --------------------------------------------- > P0(int *x, int *y, atomic_t *z) > { > int r0; > > WRITE_ONCE(*x, 1); > r0 = atomic_add_unless(z,1,5); > WRITE_ONCE(*y, 1); > } > > P1(int *x, int *y) > { > int r0; > > r0 = READ_ONCE(*y); > if (r0 == 1) > WRITE_ONCE(*x, 2); > } > > exists (1:r0=1 /\ x=1) > --------------------------------------------- > Should z also be changed from atomic_t to int? ^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: [PATCH v3 4/5] tools/memory-model: Switch to softcoded herd7 tags 2024-09-21 7:39 ` Jonas Oberhauser @ 2024-09-21 11:28 ` Akira Yokosawa 0 siblings, 0 replies; 10+ messages in thread From: Akira Yokosawa @ 2024-09-21 11:28 UTC (permalink / raw) To: Jonas Oberhauser, paulmck Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget, dlustig, joel, urezki, quic_neeraju, frederic, linux-kernel, lkmm, hernan.poncedeleon, Akira Yokosawa Hi, On Sat, 21 Sep 2024 09:39:05 +0200, Jonas Oberhauser wrote: > Thanks Akira for your continued eagle eyes! > Will include in next revision. > > One question below. > jonas > > > > Am 9/21/2024 um 4:44 AM schrieb Akira Yokosawa: >> This litmus test is not compatible with klitmus7, which is much >> stricter than herd7's C parser. >> >> You can have only int or int* variables in the exists clause. I should have said: By default, you can have only int or int* variables in the exists clause. You can find an example where an atomic_t variable is listed in its exists clause at: Documentation/litmus-tests/atomic/Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus , where the atomic_t variable is declared explicitly in the initialization block as follows: { atomic_t v = ATOMIC_INIT(1); } >> Register variables need their declarations at the top of each Pn() >> (classic C). >> >> See below for klitmus7 ready code. >> >> And tools/memory-model/litmus-tests/README need to mention this >> litmus test. >> >> Thanks, Akira >> >> --------------------------------------------- >> P0(int *x, int *y, atomic_t *z) >> { >> int r0; >> >> WRITE_ONCE(*x, 1); >> r0 = atomic_add_unless(z,1,5); >> WRITE_ONCE(*y, 1); >> } >> >> P1(int *x, int *y) >> { >> int r0; >> >> r0 = READ_ONCE(*y); >> if (r0 == 1) >> WRITE_ONCE(*x, 2); >> } >> >> exists (1:r0=1 /\ x=1) >> --------------------------------------------- >> > > Should z also be changed from atomic_t to int? > No, it should not. Such a change would make z incompatible with atomic_add_unless(). Thanks, Akira ^ permalink raw reply [flat|nested] 10+ messages in thread
* [PATCH v3 5/5] tools/memory-model: Distinguish between syntactic and semantic tags 2024-09-19 13:06 [PATCH v3 0/5] tools/memory-model: Define more of LKMM in tools/memory-model Jonas Oberhauser ` (3 preceding siblings ...) 2024-09-19 13:06 ` [PATCH v3 4/5] tools/memory-model: Switch to softcoded herd7 tags Jonas Oberhauser @ 2024-09-19 13:06 ` Jonas Oberhauser 4 siblings, 0 replies; 10+ messages in thread From: Jonas Oberhauser @ 2024-09-19 13:06 UTC (permalink / raw) To: paulmck Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget, akiyks, dlustig, joel, urezki, quic_neeraju, frederic, linux-kernel, lkmm, hernan.poncedeleon, Jonas Oberhauser Not all tags that are always there syntactically also provide semantic membership in the corresponding set. 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 <boqun.feng@gmail.com> Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com> --- tools/memory-model/linux-kernel.bell | 22 +-- tools/memory-model/linux-kernel.def | 198 +++++++++++++-------------- 2 files changed, 110 insertions(+), 110 deletions(-) diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell index 703028e5e091..dd49b987704d 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 4281572732bd..2b3a12c55f93 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) \ No newline at end of file +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) \ No newline at end of file -- 2.34.1 ^ permalink raw reply [flat|nested] 10+ messages in thread
end of thread, other threads:[~2024-09-21 11:28 UTC | newest] Thread overview: 10+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2024-09-19 13:06 [PATCH v3 0/5] tools/memory-model: Define more of LKMM in tools/memory-model Jonas Oberhauser 2024-09-19 13:06 ` [PATCH v3 1/5] tools/memory-model: Legitimize current use of tags in LKMM macros Jonas Oberhauser 2024-09-19 13:06 ` [PATCH v3 2/5] tools/memory-model: Define applicable tags on operation in tools/ Jonas Oberhauser 2024-09-19 13:06 ` [PATCH v3 3/5] tools/memory-model: Define effect of Mb tags on RMWs " Jonas Oberhauser 2024-09-19 13:06 ` [PATCH v3 4/5] tools/memory-model: Switch to softcoded herd7 tags Jonas Oberhauser 2024-09-20 12:23 ` Hernan Ponce de Leon 2024-09-21 2:44 ` Akira Yokosawa 2024-09-21 7:39 ` Jonas Oberhauser 2024-09-21 11:28 ` Akira Yokosawa 2024-09-19 13:06 ` [PATCH v3 5/5] tools/memory-model: Distinguish between syntactic and semantic tags Jonas Oberhauser
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox
all inboxes | Powered by JetHome®