* [PATCH v4 0/5] tools/memory-model: Define more of LKMM in tools/memory-model
@ 2024-09-30 10:57 Jonas Oberhauser
2024-09-30 10:57 ` [PATCH v4 1/5] tools/memory-model: Legitimize current use of tags in LKMM macros Jonas Oberhauser
` (5 more replies)
0 siblings, 6 replies; 35+ messages in thread
From: Jonas Oberhauser @ 2024-09-30 10:57 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
Changes from v3 to v4:
- removed a litmus test (submitted to Paul's larger test repo instead)
- fixed several formatting/naming issues pointed out by Akira
- updated the reference herd version number in memory-model/README.md.
*Note*: this may need to be retouched after herd is updated.
I also did not update the table under klitmus7 compatibility, which
I took to refer only to klitmus7, although its header is "herdtools7"
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/README | 2 +-
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 +++++++++---------
6 files changed, 150 insertions(+), 119 deletions(-)
--
2.34.1
^ permalink raw reply [flat|nested] 35+ messages in thread
* [PATCH v4 1/5] tools/memory-model: Legitimize current use of tags in LKMM macros
2024-09-30 10:57 [PATCH v4 0/5] tools/memory-model: Define more of LKMM in tools/memory-model Jonas Oberhauser
@ 2024-09-30 10:57 ` Jonas Oberhauser
2024-10-28 22:11 ` Boqun Feng
2024-09-30 10:57 ` [PATCH v4 2/5] tools/memory-model: Define applicable tags on operation in tools/ Jonas Oberhauser
` (4 subsequent siblings)
5 siblings, 1 reply; 35+ messages in thread
From: Jonas Oberhauser @ 2024-09-30 10:57 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] 35+ messages in thread
* [PATCH v4 2/5] tools/memory-model: Define applicable tags on operation in tools/...
2024-09-30 10:57 [PATCH v4 0/5] tools/memory-model: Define more of LKMM in tools/memory-model Jonas Oberhauser
2024-09-30 10:57 ` [PATCH v4 1/5] tools/memory-model: Legitimize current use of tags in LKMM macros Jonas Oberhauser
@ 2024-09-30 10:57 ` Jonas Oberhauser
2024-10-28 22:12 ` Boqun Feng
2024-09-30 10:57 ` [PATCH v4 3/5] tools/memory-model: Define effect of Mb tags on RMWs " Jonas Oberhauser
` (3 subsequent siblings)
5 siblings, 1 reply; 35+ messages in thread
From: Jonas Oberhauser @ 2024-09-30 10:57 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] 35+ messages in thread
* [PATCH v4 3/5] tools/memory-model: Define effect of Mb tags on RMWs in tools/...
2024-09-30 10:57 [PATCH v4 0/5] tools/memory-model: Define more of LKMM in tools/memory-model Jonas Oberhauser
2024-09-30 10:57 ` [PATCH v4 1/5] tools/memory-model: Legitimize current use of tags in LKMM macros Jonas Oberhauser
2024-09-30 10:57 ` [PATCH v4 2/5] tools/memory-model: Define applicable tags on operation in tools/ Jonas Oberhauser
@ 2024-09-30 10:57 ` Jonas Oberhauser
2024-10-28 22:15 ` Boqun Feng
2024-09-30 10:57 ` [PATCH v4 4/5] tools/memory-model: Switch to softcoded herd7 tags Jonas Oberhauser
` (2 subsequent siblings)
5 siblings, 1 reply; 35+ messages in thread
From: Jonas Oberhauser @ 2024-09-30 10:57 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] 35+ messages in thread
* [PATCH v4 4/5] tools/memory-model: Switch to softcoded herd7 tags
2024-09-30 10:57 [PATCH v4 0/5] tools/memory-model: Define more of LKMM in tools/memory-model Jonas Oberhauser
` (2 preceding siblings ...)
2024-09-30 10:57 ` [PATCH v4 3/5] tools/memory-model: Define effect of Mb tags on RMWs " Jonas Oberhauser
@ 2024-09-30 10:57 ` Jonas Oberhauser
2024-10-02 17:34 ` Hernan Ponce de Leon
2024-10-29 0:04 ` Boqun Feng
2024-09-30 10:57 ` [PATCH v4 5/5] tools/memory-model: Distinguish between syntactic and semantic tags Jonas Oberhauser
2024-10-28 20:16 ` [PATCH v4 0/5] tools/memory-model: Define more of LKMM in tools/memory-model Paul E. McKenney
5 siblings, 2 replies; 35+ messages in thread
From: Jonas Oberhauser @ 2024-09-30 10:57 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 -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.
(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/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(-)
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)
--
2.34.1
^ permalink raw reply [flat|nested] 35+ messages in thread
* [PATCH v4 5/5] tools/memory-model: Distinguish between syntactic and semantic tags
2024-09-30 10:57 [PATCH v4 0/5] tools/memory-model: Define more of LKMM in tools/memory-model Jonas Oberhauser
` (3 preceding siblings ...)
2024-09-30 10:57 ` [PATCH v4 4/5] tools/memory-model: Switch to softcoded herd7 tags Jonas Oberhauser
@ 2024-09-30 10:57 ` Jonas Oberhauser
2024-10-29 0:15 ` Boqun Feng
2024-10-28 20:16 ` [PATCH v4 0/5] tools/memory-model: Define more of LKMM in tools/memory-model Paul E. McKenney
5 siblings, 1 reply; 35+ messages in thread
From: Jonas Oberhauser @ 2024-09-30 10:57 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 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)
--
2.34.1
^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: [PATCH v4 4/5] tools/memory-model: Switch to softcoded herd7 tags
2024-09-30 10:57 ` [PATCH v4 4/5] tools/memory-model: Switch to softcoded herd7 tags Jonas Oberhauser
@ 2024-10-02 17:34 ` Hernan Ponce de Leon
2024-10-29 0:04 ` Boqun Feng
1 sibling, 0 replies; 35+ messages in thread
From: Hernan Ponce de Leon @ 2024-10-02 17:34 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/30/2024 12:57 PM, Jonas Oberhauser wrote:
> 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.
The changes required for this patch were already merged to herd7.
>
> 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.
>
> (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/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(-)
>
> 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)
^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: [PATCH v4 0/5] tools/memory-model: Define more of LKMM in tools/memory-model
2024-09-30 10:57 [PATCH v4 0/5] tools/memory-model: Define more of LKMM in tools/memory-model Jonas Oberhauser
` (4 preceding siblings ...)
2024-09-30 10:57 ` [PATCH v4 5/5] tools/memory-model: Distinguish between syntactic and semantic tags Jonas Oberhauser
@ 2024-10-28 20:16 ` Paul E. McKenney
2024-11-10 15:17 ` Akira Yokosawa
5 siblings, 1 reply; 35+ messages in thread
From: Paul E. McKenney @ 2024-10-28 20:16 UTC (permalink / raw)
To: Jonas Oberhauser
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
On Mon, Sep 30, 2024 at 12:57:05PM +0200, Jonas Oberhauser wrote:
> 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.
Thank you, Jonas!
Queued for further review and testing. This does need at least an ack to
proceed to mainline (hint to LKMM maintainers).
Thanx, Paul
> 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
>
> Changes from v3 to v4:
> - removed a litmus test (submitted to Paul's larger test repo instead)
> - fixed several formatting/naming issues pointed out by Akira
> - updated the reference herd version number in memory-model/README.md.
> *Note*: this may need to be retouched after herd is updated.
> I also did not update the table under klitmus7 compatibility, which
> I took to refer only to klitmus7, although its header is "herdtools7"
>
>
>
> 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/README | 2 +-
> 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 +++++++++---------
> 6 files changed, 150 insertions(+), 119 deletions(-)
>
> --
> 2.34.1
>
^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: [PATCH v4 1/5] tools/memory-model: Legitimize current use of tags in LKMM macros
2024-09-30 10:57 ` [PATCH v4 1/5] tools/memory-model: Legitimize current use of tags in LKMM macros Jonas Oberhauser
@ 2024-10-28 22:11 ` Boqun Feng
0 siblings, 0 replies; 35+ messages in thread
From: Boqun Feng @ 2024-10-28 22:11 UTC (permalink / raw)
To: Jonas Oberhauser
Cc: paulmck, stern, parri.andrea, will, peterz, npiggin, dhowells,
j.alglave, luc.maranget, akiyks, dlustig, joel, urezki,
quic_neeraju, frederic, linux-kernel, lkmm, hernan.poncedeleon
On Mon, Sep 30, 2024 at 12:57:06PM +0200, Jonas Oberhauser wrote:
> 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>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Regards,
Boqun
> ---
> 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] 35+ messages in thread
* Re: [PATCH v4 2/5] tools/memory-model: Define applicable tags on operation in tools/...
2024-09-30 10:57 ` [PATCH v4 2/5] tools/memory-model: Define applicable tags on operation in tools/ Jonas Oberhauser
@ 2024-10-28 22:12 ` Boqun Feng
0 siblings, 0 replies; 35+ messages in thread
From: Boqun Feng @ 2024-10-28 22:12 UTC (permalink / raw)
To: Jonas Oberhauser
Cc: paulmck, stern, parri.andrea, will, peterz, npiggin, dhowells,
j.alglave, luc.maranget, akiyks, dlustig, joel, urezki,
quic_neeraju, frederic, linux-kernel, lkmm, hernan.poncedeleon
On Mon, Sep 30, 2024 at 12:57:07PM +0200, Jonas Oberhauser wrote:
> 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>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Regards,
Boqun
> ---
> 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] 35+ messages in thread
* Re: [PATCH v4 3/5] tools/memory-model: Define effect of Mb tags on RMWs in tools/...
2024-09-30 10:57 ` [PATCH v4 3/5] tools/memory-model: Define effect of Mb tags on RMWs " Jonas Oberhauser
@ 2024-10-28 22:15 ` Boqun Feng
0 siblings, 0 replies; 35+ messages in thread
From: Boqun Feng @ 2024-10-28 22:15 UTC (permalink / raw)
To: Jonas Oberhauser
Cc: paulmck, stern, parri.andrea, will, peterz, npiggin, dhowells,
j.alglave, luc.maranget, akiyks, dlustig, joel, urezki,
quic_neeraju, frederic, linux-kernel, lkmm, hernan.poncedeleon,
Viktor Vafeiadis
On Mon, Sep 30, 2024 at 12:57:08PM +0200, Jonas Oberhauser wrote:
> 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>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Regards,
Boqun
> ---
> 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] 35+ messages in thread
* Re: [PATCH v4 4/5] tools/memory-model: Switch to softcoded herd7 tags
2024-09-30 10:57 ` [PATCH v4 4/5] tools/memory-model: Switch to softcoded herd7 tags Jonas Oberhauser
2024-10-02 17:34 ` Hernan Ponce de Leon
@ 2024-10-29 0:04 ` Boqun Feng
2024-10-29 23:42 ` Paul E. McKenney
2024-10-30 11:50 ` Jonas Oberhauser
1 sibling, 2 replies; 35+ messages in thread
From: Boqun Feng @ 2024-10-29 0:04 UTC (permalink / raw)
To: Jonas Oberhauser
Cc: paulmck, stern, parri.andrea, will, peterz, npiggin, dhowells,
j.alglave, luc.maranget, akiyks, dlustig, joel, urezki,
quic_neeraju, frederic, linux-kernel, lkmm, hernan.poncedeleon
On Mon, Sep 30, 2024 at 12:57:09PM +0200, Jonas Oberhauser wrote:
> 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.
>
> (To be) Signed-off-by: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>
> Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
One bit below:
> ---
> .../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(-)
>
> 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] |
Not in this patch, but don't you need to update this again to all cap
to match your changes in patch #5? ;-)
Regards,
Boqun
> | 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)
> --
> 2.34.1
>
>
^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: [PATCH v4 5/5] tools/memory-model: Distinguish between syntactic and semantic tags
2024-09-30 10:57 ` [PATCH v4 5/5] tools/memory-model: Distinguish between syntactic and semantic tags Jonas Oberhauser
@ 2024-10-29 0:15 ` Boqun Feng
2024-10-29 23:41 ` Paul E. McKenney
0 siblings, 1 reply; 35+ messages in thread
From: Boqun Feng @ 2024-10-29 0:15 UTC (permalink / raw)
To: Jonas Oberhauser
Cc: paulmck, stern, parri.andrea, will, peterz, npiggin, dhowells,
j.alglave, luc.maranget, akiyks, dlustig, joel, urezki,
quic_neeraju, frederic, linux-kernel, lkmm, hernan.poncedeleon
On Mon, Sep 30, 2024 at 12:57:10PM +0200, Jonas Oberhauser wrote:
> Not all tags that are always there syntactically also provide semantic
> membership in the corresponding set. For example, an 'acquire tag on a
Maybe:
Not all annotated accesses provide the same semantic as their syntactic
tags...
?
> 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>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
I've tested this series with the following herd version:
7.57+1, Rev: 8e7e63cd400e3eae8eac22dfdbd9dae0f243319b
all the litmus tests in the litmus-tests/ and all the litmus tests
downloaded and tested by scripts/checkghlitmus.sh (expected two tests
with smp_memb()) passed. So feel free to add:
Tested-by: Boqun Feng <boqun.feng@gmail.com>
Regards,
Boqun
> ---
> 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 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)
> --
> 2.34.1
>
>
^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: [PATCH v4 5/5] tools/memory-model: Distinguish between syntactic and semantic tags
2024-10-29 0:15 ` Boqun Feng
@ 2024-10-29 23:41 ` Paul E. McKenney
2024-10-30 11:38 ` Jonas Oberhauser
0 siblings, 1 reply; 35+ messages in thread
From: Paul E. McKenney @ 2024-10-29 23:41 UTC (permalink / raw)
To: Boqun Feng
Cc: Jonas Oberhauser, stern, parri.andrea, will, peterz, npiggin,
dhowells, j.alglave, luc.maranget, akiyks, dlustig, joel, urezki,
quic_neeraju, frederic, linux-kernel, lkmm, hernan.poncedeleon
On Mon, Oct 28, 2024 at 05:15:46PM -0700, Boqun Feng wrote:
> On Mon, Sep 30, 2024 at 12:57:10PM +0200, Jonas Oberhauser wrote:
> > Not all tags that are always there syntactically also provide semantic
> > membership in the corresponding set. For example, an 'acquire tag on a
>
> Maybe:
>
> Not all annotated accesses provide the same semantic as their syntactic
> tags...
>
> ?
Jonas, are you OK with this change? If so, I can apply it on my next
rebase.
> > 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>
>
> Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
>
> I've tested this series with the following herd version:
>
> 7.57+1, Rev: 8e7e63cd400e3eae8eac22dfdbd9dae0f243319b
>
> all the litmus tests in the litmus-tests/ and all the litmus tests
> downloaded and tested by scripts/checkghlitmus.sh (expected two tests
> with smp_memb()) passed. So feel free to add:
>
> Tested-by: Boqun Feng <boqun.feng@gmail.com>
Thank you, Boqun! I have applied your two tags to all five commits.
Thanx, Paul
> Regards,
> Boqun
>
> > ---
> > 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 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)
> > --
> > 2.34.1
> >
> >
^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: [PATCH v4 4/5] tools/memory-model: Switch to softcoded herd7 tags
2024-10-29 0:04 ` Boqun Feng
@ 2024-10-29 23:42 ` Paul E. McKenney
2024-10-30 11:50 ` Jonas Oberhauser
1 sibling, 0 replies; 35+ messages in thread
From: Paul E. McKenney @ 2024-10-29 23:42 UTC (permalink / raw)
To: Boqun Feng
Cc: Jonas Oberhauser, stern, parri.andrea, will, peterz, npiggin,
dhowells, j.alglave, luc.maranget, akiyks, dlustig, joel, urezki,
quic_neeraju, frederic, linux-kernel, lkmm, hernan.poncedeleon
On Mon, Oct 28, 2024 at 05:04:38PM -0700, Boqun Feng wrote:
> On Mon, Sep 30, 2024 at 12:57:09PM +0200, Jonas Oberhauser wrote:
> > 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.
> >
> > (To be) Signed-off-by: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>
> > Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
>
> Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
>
> One bit below:
Jonas, if you agree, please feel free to send this as an updated patch
5/5 or as a separate patch. Either way, just let me know!
Thanx, Paul
> > ---
> > .../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(-)
> >
> > 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] |
>
> Not in this patch, but don't you need to update this again to all cap
> to match your changes in patch #5? ;-)
>
> Regards,
> Boqun
>
> > | 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)
> > --
> > 2.34.1
> >
> >
^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: [PATCH v4 5/5] tools/memory-model: Distinguish between syntactic and semantic tags
2024-10-29 23:41 ` Paul E. McKenney
@ 2024-10-30 11:38 ` Jonas Oberhauser
2024-10-30 14:34 ` Boqun Feng
0 siblings, 1 reply; 35+ messages in thread
From: Jonas Oberhauser @ 2024-10-30 11:38 UTC (permalink / raw)
To: paulmck, Boqun Feng
Cc: stern, parri.andrea, will, peterz, npiggin, dhowells, j.alglave,
luc.maranget, akiyks, dlustig, joel, urezki, quic_neeraju,
frederic, linux-kernel, lkmm, hernan.poncedeleon
Am 10/30/2024 um 12:41 AM schrieb Paul E. McKenney:
> On Mon, Oct 28, 2024 at 05:15:46PM -0700, Boqun Feng wrote:
>> On Mon, Sep 30, 2024 at 12:57:10PM +0200, Jonas Oberhauser wrote:
>>> Not all tags that are always there syntactically also provide semantic
>>> membership in the corresponding set. For example, an 'acquire tag on a
>>
>> Maybe:
>>
>> Not all annotated accesses provide the same semantic as their syntactic
>> tags...
>>
>> ?
>
> Jonas, are you OK with this change? If so, I can apply it on my next
> rebase.
>
I'm ok with an extra s after semantics and a minor rephrase:
Not all annotated accesses provide the semantics their syntactic
tags would imply
What do you think @Boqun ?
jonas
^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: [PATCH v4 4/5] tools/memory-model: Switch to softcoded herd7 tags
2024-10-29 0:04 ` Boqun Feng
2024-10-29 23:42 ` Paul E. McKenney
@ 2024-10-30 11:50 ` Jonas Oberhauser
2024-10-30 13:46 ` Paul E. McKenney
1 sibling, 1 reply; 35+ messages in thread
From: Jonas Oberhauser @ 2024-10-30 11:50 UTC (permalink / raw)
To: Boqun Feng
Cc: paulmck, stern, parri.andrea, will, peterz, npiggin, dhowells,
j.alglave, luc.maranget, akiyks, dlustig, joel, urezki,
quic_neeraju, frederic, linux-kernel, lkmm, hernan.poncedeleon
Am 10/29/2024 um 1:04 AM schrieb Boqun Feng:
>
> One bit below:
>
> On Mon, Sep 30, 2024 at 12:57:09PM +0200, Jonas Oberhauser wrote:
>> ------------------------------------------------------------------------------
>> | RMW ops w/o return value | |
>> ------------------------------------------------------------------------------
>> - | atomic_add | R*[noreturn] ->rmw W*[once] |
>> + | atomic_add | R*[noreturn] ->rmw W*[noreturn] |
>
> Not in this patch, but don't you need to update this again to all cap
> to match your changes in patch #5? ;-)
>
Hmmm, probably that is a good idea.
I actually had thought about it for some of the other places in the doc
that mention the tags, and concluded that we'll just use the semantic
tags there.
But in fact, this file is about the syntactic representation in herd,
and there is no noreturn semantic tag on the W*, so it wouldn't match it
even if it were correct.
So I think this needs to be addressed in 5/5.
jonas
^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: [PATCH v4 4/5] tools/memory-model: Switch to softcoded herd7 tags
2024-10-30 11:50 ` Jonas Oberhauser
@ 2024-10-30 13:46 ` Paul E. McKenney
0 siblings, 0 replies; 35+ messages in thread
From: Paul E. McKenney @ 2024-10-30 13:46 UTC (permalink / raw)
To: Jonas Oberhauser
Cc: Boqun Feng, stern, parri.andrea, will, peterz, npiggin, dhowells,
j.alglave, luc.maranget, akiyks, dlustig, joel, urezki,
quic_neeraju, frederic, linux-kernel, lkmm, hernan.poncedeleon
On Wed, Oct 30, 2024 at 12:50:19PM +0100, Jonas Oberhauser wrote:
>
>
> Am 10/29/2024 um 1:04 AM schrieb Boqun Feng:
> >
> > One bit below:
> >
> > On Mon, Sep 30, 2024 at 12:57:09PM +0200, Jonas Oberhauser wrote:
> > > ------------------------------------------------------------------------------
> > > | RMW ops w/o return value | |
> > > ------------------------------------------------------------------------------
> > > - | atomic_add | R*[noreturn] ->rmw W*[once] |
> > > + | atomic_add | R*[noreturn] ->rmw W*[noreturn] |
> >
> > Not in this patch, but don't you need to update this again to all cap
> > to match your changes in patch #5? ;-)
> >
>
> Hmmm, probably that is a good idea.
> I actually had thought about it for some of the other places in the doc that
> mention the tags, and concluded that we'll just use the semantic tags there.
>
> But in fact, this file is about the syntactic representation in herd, and
> there is no noreturn semantic tag on the W*, so it wouldn't match it even if
> it were correct.
>
> So I think this needs to be addressed in 5/5.
Thank you for checking!
Please send me either a replacement for 5/5 or a patch for me to fold
into 5/5.
Thanx, Paul
^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: [PATCH v4 5/5] tools/memory-model: Distinguish between syntactic and semantic tags
2024-10-30 11:38 ` Jonas Oberhauser
@ 2024-10-30 14:34 ` Boqun Feng
2024-10-30 16:27 ` Paul E. McKenney
2024-11-05 20:21 ` Paul E. McKenney
0 siblings, 2 replies; 35+ messages in thread
From: Boqun Feng @ 2024-10-30 14:34 UTC (permalink / raw)
To: Jonas Oberhauser
Cc: paulmck, stern, parri.andrea, will, peterz, npiggin, dhowells,
j.alglave, luc.maranget, akiyks, dlustig, joel, urezki,
quic_neeraju, frederic, linux-kernel, lkmm, hernan.poncedeleon
On Wed, Oct 30, 2024 at 12:38:26PM +0100, Jonas Oberhauser wrote:
>
>
> Am 10/30/2024 um 12:41 AM schrieb Paul E. McKenney:
> > On Mon, Oct 28, 2024 at 05:15:46PM -0700, Boqun Feng wrote:
> > > On Mon, Sep 30, 2024 at 12:57:10PM +0200, Jonas Oberhauser wrote:
> > > > Not all tags that are always there syntactically also provide semantic
> > > > membership in the corresponding set. For example, an 'acquire tag on a
> > >
> > > Maybe:
> > >
> > > Not all annotated accesses provide the same semantic as their syntactic
> > > tags...
> > >
> > > ?
> >
> > Jonas, are you OK with this change? If so, I can apply it on my next
> > rebase.
> >
>
> I'm ok with an extra s after semantics and a minor rephrase:
>
> Not all annotated accesses provide the semantics their syntactic
> tags would imply
>
>
> What do you think @Boqun ?
>
Yes, of course! This looks good to me.
Regards,
Boqun
>
> jonas
>
^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: [PATCH v4 5/5] tools/memory-model: Distinguish between syntactic and semantic tags
2024-10-30 14:34 ` Boqun Feng
@ 2024-10-30 16:27 ` Paul E. McKenney
2024-11-05 20:21 ` Paul E. McKenney
1 sibling, 0 replies; 35+ messages in thread
From: Paul E. McKenney @ 2024-10-30 16:27 UTC (permalink / raw)
To: Boqun Feng
Cc: Jonas Oberhauser, stern, parri.andrea, will, peterz, npiggin,
dhowells, j.alglave, luc.maranget, akiyks, dlustig, joel, urezki,
quic_neeraju, frederic, linux-kernel, lkmm, hernan.poncedeleon
On Wed, Oct 30, 2024 at 07:34:45AM -0700, Boqun Feng wrote:
> On Wed, Oct 30, 2024 at 12:38:26PM +0100, Jonas Oberhauser wrote:
> >
> >
> > Am 10/30/2024 um 12:41 AM schrieb Paul E. McKenney:
> > > On Mon, Oct 28, 2024 at 05:15:46PM -0700, Boqun Feng wrote:
> > > > On Mon, Sep 30, 2024 at 12:57:10PM +0200, Jonas Oberhauser wrote:
> > > > > Not all tags that are always there syntactically also provide semantic
> > > > > membership in the corresponding set. For example, an 'acquire tag on a
> > > >
> > > > Maybe:
> > > >
> > > > Not all annotated accesses provide the same semantic as their syntactic
> > > > tags...
> > > >
> > > > ?
> > >
> > > Jonas, are you OK with this change? If so, I can apply it on my next
> > > rebase.
> >
> > I'm ok with an extra s after semantics and a minor rephrase:
> >
> > Not all annotated accesses provide the semantics their syntactic
> > tags would imply
> >
> > What do you think @Boqun ?
>
> Yes, of course! This looks good to me.
Very good!
This is in the commit that you (Jonas) will fix, correct? If so, could
you please make this update as well? Otherwise, Murphy being who he is,
I will end up changing this and then overwriting my change with your
updated commit. ;-)
Thanx, Paul
^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: [PATCH v4 5/5] tools/memory-model: Distinguish between syntactic and semantic tags
2024-10-30 14:34 ` Boqun Feng
2024-10-30 16:27 ` Paul E. McKenney
@ 2024-11-05 20:21 ` Paul E. McKenney
2024-11-06 10:28 ` Jonas Oberhauser
1 sibling, 1 reply; 35+ messages in thread
From: Paul E. McKenney @ 2024-11-05 20:21 UTC (permalink / raw)
To: Boqun Feng
Cc: Jonas Oberhauser, stern, parri.andrea, will, peterz, npiggin,
dhowells, j.alglave, luc.maranget, akiyks, dlustig, joel, urezki,
quic_neeraju, frederic, linux-kernel, lkmm, hernan.poncedeleon
On Wed, Oct 30, 2024 at 07:34:45AM -0700, Boqun Feng wrote:
> On Wed, Oct 30, 2024 at 12:38:26PM +0100, Jonas Oberhauser wrote:
> >
> >
> > Am 10/30/2024 um 12:41 AM schrieb Paul E. McKenney:
> > > On Mon, Oct 28, 2024 at 05:15:46PM -0700, Boqun Feng wrote:
> > > > On Mon, Sep 30, 2024 at 12:57:10PM +0200, Jonas Oberhauser wrote:
> > > > > Not all tags that are always there syntactically also provide semantic
> > > > > membership in the corresponding set. For example, an 'acquire tag on a
> > > >
> > > > Maybe:
> > > >
> > > > Not all annotated accesses provide the same semantic as their syntactic
> > > > tags...
> > > >
> > > > ?
> > >
> > > Jonas, are you OK with this change? If so, I can apply it on my next
> > > rebase.
> > >
> >
> > I'm ok with an extra s after semantics and a minor rephrase:
> >
> > Not all annotated accesses provide the semantics their syntactic
> > tags would imply
> >
> > What do you think @Boqun ?
>
> Yes, of course! This looks good to me.
Please see below for what I currently have. If there are no objections
in a day or so, I will set up these five commits for the upcoming v6.13
merge window.
The additional bit pointed out by Boqun [1] can be addressed by a
separate commit.
Thanx, Paul
[1] https://lore.kernel.org/all/ZyAmlh5GDBsqY0sZ@Boquns-Mac-mini.local/
------------------------------------------------------------------------
commit c53d54ed7e40255ea0ea66dd121672fd22423326
Author: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Date: Mon Sep 30 12:57:10 2024 +0200
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 <boqun.feng@gmail.com>
Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Tested-by: Boqun Feng <boqun.feng@gmail.com>
diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
index 8ae47545df978..fe65998002b99 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 d7279a357cba0..49e402782e49c 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)
^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: [PATCH v4 5/5] tools/memory-model: Distinguish between syntactic and semantic tags
2024-11-05 20:21 ` Paul E. McKenney
@ 2024-11-06 10:28 ` Jonas Oberhauser
2024-11-06 15:04 ` Paul E. McKenney
0 siblings, 1 reply; 35+ messages in thread
From: Jonas Oberhauser @ 2024-11-06 10:28 UTC (permalink / raw)
To: paulmck, Boqun Feng
Cc: stern, parri.andrea, will, peterz, npiggin, dhowells, j.alglave,
luc.maranget, akiyks, dlustig, joel, urezki, quic_neeraju,
frederic, linux-kernel, lkmm, hernan.poncedeleon
Am 11/5/2024 um 9:21 PM schrieb Paul E. McKenney:
> On Wed, Oct 30, 2024 at 07:34:45AM -0700, Boqun Feng wrote:
>> On Wed, Oct 30, 2024 at 12:38:26PM +0100, Jonas Oberhauser wrote:
>>>
>>>
>>> Am 10/30/2024 um 12:41 AM schrieb Paul E. McKenney:
>>>> On Mon, Oct 28, 2024 at 05:15:46PM -0700, Boqun Feng wrote:
>>>>> On Mon, Sep 30, 2024 at 12:57:10PM +0200, Jonas Oberhauser wrote:
>>>>>> Not all tags that are always there syntactically also provide semantic
>>>>>> membership in the corresponding set. For example, an 'acquire tag on a
>>>>>
>>>>> Maybe:
>>>>>
>>>>> Not all annotated accesses provide the same semantic as their syntactic
>>>>> tags...
>>>>>
>>>>> ?
>>>>
>>>> Jonas, are you OK with this change? If so, I can apply it on my next
>>>> rebase.
>>>>
>>>
>>> I'm ok with an extra s after semantics and a minor rephrase:
>>>
>>> Not all annotated accesses provide the semantics their syntactic
>>> tags would imply
>>>
>>> What do you think @Boqun ?
>>
>> Yes, of course! This looks good to me.
>
> Please see below for what I currently have. If there are no objections
> in a day or so, I will set up these five commits for the upcoming v6.13
> merge window.
>
> The additional bit pointed out by Boqun [1] can be addressed by a
> separate commit.
>
> Thanx, Paul
>
> [1] https://lore.kernel.org/all/ZyAmlh5GDBsqY0sZ@Boquns-Mac-mini.local/
I'm confused, did I forget to add the fix to the capitalization issue
discovered by Boqun to the fixed commit? I vividly remember typing git
commit add ...
jonas
^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: [PATCH v4 5/5] tools/memory-model: Distinguish between syntactic and semantic tags
2024-11-06 10:28 ` Jonas Oberhauser
@ 2024-11-06 15:04 ` Paul E. McKenney
2024-11-06 18:00 ` Paul E. McKenney
0 siblings, 1 reply; 35+ messages in thread
From: Paul E. McKenney @ 2024-11-06 15:04 UTC (permalink / raw)
To: Jonas Oberhauser
Cc: Boqun Feng, stern, parri.andrea, will, peterz, npiggin, dhowells,
j.alglave, luc.maranget, akiyks, dlustig, joel, urezki,
quic_neeraju, frederic, linux-kernel, lkmm, hernan.poncedeleon
On Wed, Nov 06, 2024 at 11:28:28AM +0100, Jonas Oberhauser wrote:
>
>
> Am 11/5/2024 um 9:21 PM schrieb Paul E. McKenney:
> > On Wed, Oct 30, 2024 at 07:34:45AM -0700, Boqun Feng wrote:
> > > On Wed, Oct 30, 2024 at 12:38:26PM +0100, Jonas Oberhauser wrote:
> > > >
> > > >
> > > > Am 10/30/2024 um 12:41 AM schrieb Paul E. McKenney:
> > > > > On Mon, Oct 28, 2024 at 05:15:46PM -0700, Boqun Feng wrote:
> > > > > > On Mon, Sep 30, 2024 at 12:57:10PM +0200, Jonas Oberhauser wrote:
> > > > > > > Not all tags that are always there syntactically also provide semantic
> > > > > > > membership in the corresponding set. For example, an 'acquire tag on a
> > > > > >
> > > > > > Maybe:
> > > > > >
> > > > > > Not all annotated accesses provide the same semantic as their syntactic
> > > > > > tags...
> > > > > >
> > > > > > ?
> > > > >
> > > > > Jonas, are you OK with this change? If so, I can apply it on my next
> > > > > rebase.
> > > > >
> > > >
> > > > I'm ok with an extra s after semantics and a minor rephrase:
> > > >
> > > > Not all annotated accesses provide the semantics their syntactic
> > > > tags would imply
> > > >
> > > > What do you think @Boqun ?
> > >
> > > Yes, of course! This looks good to me.
> >
> > Please see below for what I currently have. If there are no objections
> > in a day or so, I will set up these five commits for the upcoming v6.13
> > merge window.
> >
> > The additional bit pointed out by Boqun [1] can be addressed by a
> > separate commit.
> >
> > Thanx, Paul
> >
> > [1] https://lore.kernel.org/all/ZyAmlh5GDBsqY0sZ@Boquns-Mac-mini.local/
>
> I'm confused, did I forget to add the fix to the capitalization issue
> discovered by Boqun to the fixed commit? I vividly remember typing git
> commit add ...
It is quite possible that I have queued an old version of the patch.
Could you please check this commit on -rcu, shown below?
c53d54ed7e40 ("tools/memory-model: Distinguish between syntactic and semantic tags")
If this is the wrong one, please point me to the right one.
Thanx, Paul
------------------------------------------------------------------------
commit c53d54ed7e40255ea0ea66dd121672fd22423326
Author: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Date: Mon Sep 30 12:57:10 2024 +0200
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 <boqun.feng@gmail.com>
Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Tested-by: Boqun Feng <boqun.feng@gmail.com>
diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
index 8ae47545df978..fe65998002b99 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 d7279a357cba0..49e402782e49c 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)
^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: [PATCH v4 5/5] tools/memory-model: Distinguish between syntactic and semantic tags
2024-11-06 15:04 ` Paul E. McKenney
@ 2024-11-06 18:00 ` Paul E. McKenney
2024-11-07 9:05 ` Jonas Oberhauser
0 siblings, 1 reply; 35+ messages in thread
From: Paul E. McKenney @ 2024-11-06 18:00 UTC (permalink / raw)
To: Jonas Oberhauser
Cc: Boqun Feng, stern, parri.andrea, will, peterz, npiggin, dhowells,
j.alglave, luc.maranget, akiyks, dlustig, joel, urezki,
quic_neeraju, frederic, linux-kernel, lkmm, hernan.poncedeleon
Never mind, I found your patch in my spam folder. Apologies, and
I thought that had been fixed. I will replace the commit with your
updated patch.
Thanx, Paul
On Wed, Nov 06, 2024 at 07:04:57AM -0800, Paul E. McKenney wrote:
> On Wed, Nov 06, 2024 at 11:28:28AM +0100, Jonas Oberhauser wrote:
> >
> >
> > Am 11/5/2024 um 9:21 PM schrieb Paul E. McKenney:
> > > On Wed, Oct 30, 2024 at 07:34:45AM -0700, Boqun Feng wrote:
> > > > On Wed, Oct 30, 2024 at 12:38:26PM +0100, Jonas Oberhauser wrote:
> > > > >
> > > > >
> > > > > Am 10/30/2024 um 12:41 AM schrieb Paul E. McKenney:
> > > > > > On Mon, Oct 28, 2024 at 05:15:46PM -0700, Boqun Feng wrote:
> > > > > > > On Mon, Sep 30, 2024 at 12:57:10PM +0200, Jonas Oberhauser wrote:
> > > > > > > > Not all tags that are always there syntactically also provide semantic
> > > > > > > > membership in the corresponding set. For example, an 'acquire tag on a
> > > > > > >
> > > > > > > Maybe:
> > > > > > >
> > > > > > > Not all annotated accesses provide the same semantic as their syntactic
> > > > > > > tags...
> > > > > > >
> > > > > > > ?
> > > > > >
> > > > > > Jonas, are you OK with this change? If so, I can apply it on my next
> > > > > > rebase.
> > > > > >
> > > > >
> > > > > I'm ok with an extra s after semantics and a minor rephrase:
> > > > >
> > > > > Not all annotated accesses provide the semantics their syntactic
> > > > > tags would imply
> > > > >
> > > > > What do you think @Boqun ?
> > > >
> > > > Yes, of course! This looks good to me.
> > >
> > > Please see below for what I currently have. If there are no objections
> > > in a day or so, I will set up these five commits for the upcoming v6.13
> > > merge window.
> > >
> > > The additional bit pointed out by Boqun [1] can be addressed by a
> > > separate commit.
> > >
> > > Thanx, Paul
> > >
> > > [1] https://lore.kernel.org/all/ZyAmlh5GDBsqY0sZ@Boquns-Mac-mini.local/
> >
> > I'm confused, did I forget to add the fix to the capitalization issue
> > discovered by Boqun to the fixed commit? I vividly remember typing git
> > commit add ...
>
> It is quite possible that I have queued an old version of the patch.
> Could you please check this commit on -rcu, shown below?
>
> c53d54ed7e40 ("tools/memory-model: Distinguish between syntactic and semantic tags")
>
> If this is the wrong one, please point me to the right one.
>
> Thanx, Paul
>
> ------------------------------------------------------------------------
>
> commit c53d54ed7e40255ea0ea66dd121672fd22423326
> Author: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
> Date: Mon Sep 30 12:57:10 2024 +0200
>
> 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 <boqun.feng@gmail.com>
> Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
> Tested-by: Boqun Feng <boqun.feng@gmail.com>
>
> diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
> index 8ae47545df978..fe65998002b99 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 d7279a357cba0..49e402782e49c 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)
^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: [PATCH v4 5/5] tools/memory-model: Distinguish between syntactic and semantic tags
2024-11-06 18:00 ` Paul E. McKenney
@ 2024-11-07 9:05 ` Jonas Oberhauser
2024-11-07 10:51 ` Akira Yokosawa
0 siblings, 1 reply; 35+ messages in thread
From: Jonas Oberhauser @ 2024-11-07 9:05 UTC (permalink / raw)
To: paulmck
Cc: Boqun Feng, stern, parri.andrea, will, peterz, npiggin, dhowells,
j.alglave, luc.maranget, akiyks, dlustig, joel, urezki,
quic_neeraju, frederic, linux-kernel, lkmm, hernan.poncedeleon
Am 11/6/2024 um 7:00 PM schrieb Paul E. McKenney:
> Never mind, I found your patch in my spam folder.
Glad that got cleared up. I had gotten very confused because you had
also responded to the thread with the patch.
> check this commit on -rcu
For future reference, where can I find the -rcu repository? I couldn't
find the commit on paulmckrcu/linux, but maybe I looked incorrectly.
Have fun,
jonas
PS:
> Apologies, and I thought that had been fixed.
One might come to the conclusion that with sufficient effort, things can
be un-fixed...
^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: [PATCH v4 5/5] tools/memory-model: Distinguish between syntactic and semantic tags
2024-11-07 9:05 ` Jonas Oberhauser
@ 2024-11-07 10:51 ` Akira Yokosawa
2024-11-07 14:04 ` Paul E. McKenney
2024-11-08 9:10 ` Jonas Oberhauser
0 siblings, 2 replies; 35+ messages in thread
From: Akira Yokosawa @ 2024-11-07 10:51 UTC (permalink / raw)
To: jonas.oberhauser
Cc: akiyks, boqun.feng, dhowells, dlustig, frederic,
hernan.poncedeleon, j.alglave, joel, linux-kernel, lkmm,
luc.maranget, npiggin, parri.andrea, paulmck, peterz,
quic_neeraju, stern, urezki, will
Jonas, despite the CC, your message has not made my gmail mbox, not even
the spam folder.
I'm replying using lore's reply link.
On Thu, 7 Nov 2024 10:05:18 +0100, Jonas Oberhauser wrote:
> Am 11/6/2024 um 7:00 PM schrieb Paul E. McKenney:
>> Never mind, I found your patch in my spam folder.
> Glad that got cleared up. I had gotten very confused because you had
> also responded to the thread with the patch.
>
> > check this commit on -rcu
>
> For future reference, where can I find the -rcu repository? I couldn't
> find the commit on paulmckrcu/linux, but maybe I looked incorrectly.
You can find your patches at:
[v4] https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu.git/commit/?id=c53d54ed7e40255ea0ea66dd121672fd22423326
[v5] https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu.git/commit/?id=9b13bea0966c498629e221c3022a591cc88d4c57
and
[v4] https://github.com/paulmckrcu/linux/commit/c53d54ed7e40255ea0ea66dd121672fd22423326
[v5] https://github.com/paulmckrcu/linux/commit/9b13bea0966c498629e221c3022a591cc88d4c57
As Paul mentioned elsewhere, the [v5] patch misses tags from Boqun at the moment.
HTH, Akira
>
>
> Have fun,
> jonas
^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: [PATCH v4 5/5] tools/memory-model: Distinguish between syntactic and semantic tags
2024-11-07 10:51 ` Akira Yokosawa
@ 2024-11-07 14:04 ` Paul E. McKenney
2024-11-08 9:10 ` Jonas Oberhauser
1 sibling, 0 replies; 35+ messages in thread
From: Paul E. McKenney @ 2024-11-07 14:04 UTC (permalink / raw)
To: Akira Yokosawa
Cc: jonas.oberhauser, boqun.feng, dhowells, dlustig, frederic,
hernan.poncedeleon, j.alglave, joel, linux-kernel, lkmm,
luc.maranget, npiggin, parri.andrea, peterz, quic_neeraju, stern,
urezki, will
On Thu, Nov 07, 2024 at 07:51:52PM +0900, Akira Yokosawa wrote:
> Jonas, despite the CC, your message has not made my gmail mbox, not even
> the spam folder.
> I'm replying using lore's reply link.
>
> On Thu, 7 Nov 2024 10:05:18 +0100, Jonas Oberhauser wrote:
> > Am 11/6/2024 um 7:00 PM schrieb Paul E. McKenney:
> >> Never mind, I found your patch in my spam folder.
> > Glad that got cleared up. I had gotten very confused because you had
> > also responded to the thread with the patch.
> >
> > > check this commit on -rcu
> >
> > For future reference, where can I find the -rcu repository? I couldn't
> > find the commit on paulmckrcu/linux, but maybe I looked incorrectly.
>
> You can find your patches at:
>
> [v4] https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu.git/commit/?id=c53d54ed7e40255ea0ea66dd121672fd22423326
> [v5] https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu.git/commit/?id=9b13bea0966c498629e221c3022a591cc88d4c57
>
> and
>
> [v4] https://github.com/paulmckrcu/linux/commit/c53d54ed7e40255ea0ea66dd121672fd22423326
> [v5] https://github.com/paulmckrcu/linux/commit/9b13bea0966c498629e221c3022a591cc88d4c57
>
> As Paul mentioned elsewhere, the [v5] patch misses tags from Boqun at the moment.
Thank you both!
Just for the record, I must sadly but emphatically agree with Jonas's
point about things getting unfixed...
Thanx, Paul
^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: [PATCH v4 5/5] tools/memory-model: Distinguish between syntactic and semantic tags
2024-11-07 10:51 ` Akira Yokosawa
2024-11-07 14:04 ` Paul E. McKenney
@ 2024-11-08 9:10 ` Jonas Oberhauser
2024-11-08 10:12 ` Akira Yokosawa
1 sibling, 1 reply; 35+ messages in thread
From: Jonas Oberhauser @ 2024-11-08 9:10 UTC (permalink / raw)
To: Akira Yokosawa
Cc: boqun.feng, dhowells, dlustig, frederic, hernan.poncedeleon,
j.alglave, joel, linux-kernel, lkmm, luc.maranget, npiggin,
parri.andrea, paulmck, peterz, quic_neeraju, stern, urezki, will
Am 11/7/2024 um 11:51 AM schrieb Akira Yokosawa:
> Jonas, despite the CC, your message has not made my gmail mbox, not even
> the spam folder.
> I'm replying using lore's reply link. >
> As Paul mentioned elsewhere, the [v5] patch misses tags from Boqun at the moment.
>
So if I supply a new revision of a patch, should I include in all the
reviewed-by of the previous patch?
I hadn't done that before (because I thought I should not add other
people's tags especially if they hadn't reviewed that specific
revision), so we may be missing *a lot* of reviewed-by...
If this is the case, I'll try to scour through the previous e-mails and
add all the missing reviewed-by.
Best wishes,
jonas
^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: [PATCH v4 5/5] tools/memory-model: Distinguish between syntactic and semantic tags
2024-11-08 9:10 ` Jonas Oberhauser
@ 2024-11-08 10:12 ` Akira Yokosawa
2024-11-08 11:07 ` Jonas Oberhauser
0 siblings, 1 reply; 35+ messages in thread
From: Akira Yokosawa @ 2024-11-08 10:12 UTC (permalink / raw)
To: Jonas Oberhauser
Cc: boqun.feng, dhowells, dlustig, frederic, hernan.poncedeleon,
j.alglave, joel, linux-kernel, lkmm, luc.maranget, npiggin,
parri.andrea, paulmck, peterz, quic_neeraju, stern, urezki, will,
Akira Yokosawa
On Fri, 8 Nov 2024 10:10:48 +0100, Jonas Oberhauser wrote:
> Am 11/7/2024 um 11:51 AM schrieb Akira Yokosawa:
>> Jonas, despite the CC, your message has not made my gmail mbox, not even
>> the spam folder.
>> I'm replying using lore's reply link. >
>> As Paul mentioned elsewhere, the [v5] patch misses tags from Boqun at the moment.
>>
>
> So if I supply a new revision of a patch, should I include in all the reviewed-by
> of the previous patch?
>
It depends.
> I hadn't done that before (because I thought I should not add other people's tags
> especially if they hadn't reviewed that specific revision), so we may be missing
> *a lot* of reviewed-by...
>
Section "Using Reported-by:, Tested-by:, Reviewed-by:, Suggested-by: and Fixes:"
of Documentation/process/submitting-patches.rst has this paragraph:
Both Tested-by and Reviewed-by tags, once received on mailing list from tester
or reviewer, should be added by author to the applicable patches when sending
next versions. However if the patch has changed substantially in following
version, these tags might not be applicable anymore and thus should be removed.
Usually removal of someone's Tested-by or Reviewed-by tags should be mentioned
in the patch changelog (after the '---' separator).
Does this help you?
> If this is the case, I'll try to scour through the previous e-mails and add
> all the missing reviewed-by.
Only if Paul asks you to do so ;-)
HTH, Akira
^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: [PATCH v4 5/5] tools/memory-model: Distinguish between syntactic and semantic tags
2024-11-08 10:12 ` Akira Yokosawa
@ 2024-11-08 11:07 ` Jonas Oberhauser
2024-11-08 18:35 ` Paul E. McKenney
0 siblings, 1 reply; 35+ messages in thread
From: Jonas Oberhauser @ 2024-11-08 11:07 UTC (permalink / raw)
To: Akira Yokosawa
Cc: boqun.feng, dhowells, dlustig, frederic, hernan.poncedeleon,
j.alglave, joel, linux-kernel, lkmm, luc.maranget, npiggin,
parri.andrea, paulmck, peterz, quic_neeraju, stern, urezki, will
Am 11/8/2024 um 11:12 AM schrieb Akira Yokosawa:
> On Fri, 8 Nov 2024 10:10:48 +0100, Jonas Oberhauser wrote:
>> I hadn't done that before (because I thought I should not add other people's tags
>> especially if they hadn't reviewed that specific revision), so we may be missing
>> *a lot* of reviewed-by...
>>
>
> Section "Using Reported-by:, Tested-by:, Reviewed-by:, Suggested-by: and Fixes:"
> of Documentation/process/submitting-patches.rst has this paragraph:
>
> Both Tested-by and Reviewed-by tags, once received on mailing list from tester
> or reviewer, should be added by author to the applicable patches when sending
> next versions. However if the patch has changed substantially in following
> version, these tags might not be applicable anymore and thus should be removed.
> Usually removal of someone's Tested-by or Reviewed-by tags should be mentioned
> in the patch changelog (after the '---' separator).
>
> Does this help you?
Thanks so much, it does. My apologies to everyone whose reviewed-by tag
I failed to add :(
I should have read that more document more carefully.
Best wishes,
jonas
^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: [PATCH v4 5/5] tools/memory-model: Distinguish between syntactic and semantic tags
2024-11-08 11:07 ` Jonas Oberhauser
@ 2024-11-08 18:35 ` Paul E. McKenney
2024-11-18 15:05 ` Paul E. McKenney
0 siblings, 1 reply; 35+ messages in thread
From: Paul E. McKenney @ 2024-11-08 18:35 UTC (permalink / raw)
To: Jonas Oberhauser
Cc: Akira Yokosawa, boqun.feng, dhowells, dlustig, frederic,
hernan.poncedeleon, j.alglave, joel, linux-kernel, lkmm,
luc.maranget, npiggin, parri.andrea, peterz, quic_neeraju, stern,
urezki, will
On Fri, Nov 08, 2024 at 12:07:43PM +0100, Jonas Oberhauser wrote:
>
>
> Am 11/8/2024 um 11:12 AM schrieb Akira Yokosawa:
> > On Fri, 8 Nov 2024 10:10:48 +0100, Jonas Oberhauser wrote:
> > > I hadn't done that before (because I thought I should not add other people's tags
> > > especially if they hadn't reviewed that specific revision), so we may be missing
> > > *a lot* of reviewed-by...
> > >
> >
> > Section "Using Reported-by:, Tested-by:, Reviewed-by:, Suggested-by: and Fixes:"
> > of Documentation/process/submitting-patches.rst has this paragraph:
> >
> > Both Tested-by and Reviewed-by tags, once received on mailing list from tester
> > or reviewer, should be added by author to the applicable patches when sending
> > next versions. However if the patch has changed substantially in following
> > version, these tags might not be applicable anymore and thus should be removed.
> > Usually removal of someone's Tested-by or Reviewed-by tags should be mentioned
> > in the patch changelog (after the '---' separator).
> >
> > Does this help you?
>
> Thanks so much, it does. My apologies to everyone whose reviewed-by tag I
> failed to add :(
>
> I should have read that more document more carefully.
No worries! The important part is your changes. The tags are easy
to add. And now you know. ;-)
Thanx, Paul
^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: [PATCH v4 0/5] tools/memory-model: Define more of LKMM in tools/memory-model
2024-10-28 20:16 ` [PATCH v4 0/5] tools/memory-model: Define more of LKMM in tools/memory-model Paul E. McKenney
@ 2024-11-10 15:17 ` Akira Yokosawa
0 siblings, 0 replies; 35+ messages in thread
From: Akira Yokosawa @ 2024-11-10 15:17 UTC (permalink / raw)
To: paulmck, luc.maranget
Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells,
j.alglave, dlustig, joel, urezki, quic_neeraju, frederic,
linux-kernel, lkmm, hernan.poncedeleon, Jonas Oberhauser,
Akira Yokosawa
Hi Paul and Luc,
On Mon, 28 Oct 2024 13:16:23 -0700, Paul E. McKenney wrote:
> On Mon, Sep 30, 2024 at 12:57:05PM +0200, Jonas Oberhauser wrote:
[...]
>> 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.
>
> Thank you, Jonas!
>
> Queued for further review and testing. This does need at least an ack to
> proceed to mainline (hint to LKMM maintainers).
Paul's lkmm.2024.11.09a branch carries these 7 commits:
1 tools/memory-model: Add atomic_and()/or()/xor() and add_negative
2 tools/memory-model: Add atomic_andnot() with its variants
3 tools/memory-model: Legitimize current use of tags in LKMM macros
4 tools/memory-model: Define applicable tags on operation in tools/...
5 tools/memory-model: Define effect of Mb tags on RMWs in tools/...
6 tools/memory-model: Switch to softcoded herd7 tags
7 tools/memory-model: Distinguish between syntactic and semantic tags
As the first commit is already incompatible with released versions of herd7,
Paul will have nothing to upstream for v6.13 unless we see a new release of
herdtoolds7 whose herd7 has those atomic RMW bitwise ops and lkmmv2 variant
support in time for the upcoming merge window.
Luc, I have no idea of herdtools7's release procedure, but is there any
chance for us to see such a release of herdtools7, preferably by the end of
November?
Thanks, Akira
^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: [PATCH v4 5/5] tools/memory-model: Distinguish between syntactic and semantic tags
2024-11-08 18:35 ` Paul E. McKenney
@ 2024-11-18 15:05 ` Paul E. McKenney
2024-11-26 15:25 ` Jonas Oberhauser
0 siblings, 1 reply; 35+ messages in thread
From: Paul E. McKenney @ 2024-11-18 15:05 UTC (permalink / raw)
To: Jonas Oberhauser
Cc: Akira Yokosawa, boqun.feng, dhowells, dlustig, frederic,
hernan.poncedeleon, j.alglave, joel, linux-kernel, lkmm,
luc.maranget, npiggin, parri.andrea, peterz, quic_neeraju, stern,
urezki, will
On Fri, Nov 08, 2024 at 10:35:24AM -0800, Paul E. McKenney wrote:
> On Fri, Nov 08, 2024 at 12:07:43PM +0100, Jonas Oberhauser wrote:
> >
> >
> > Am 11/8/2024 um 11:12 AM schrieb Akira Yokosawa:
> > > On Fri, 8 Nov 2024 10:10:48 +0100, Jonas Oberhauser wrote:
> > > > I hadn't done that before (because I thought I should not add other people's tags
> > > > especially if they hadn't reviewed that specific revision), so we may be missing
> > > > *a lot* of reviewed-by...
> > > >
> > >
> > > Section "Using Reported-by:, Tested-by:, Reviewed-by:, Suggested-by: and Fixes:"
> > > of Documentation/process/submitting-patches.rst has this paragraph:
> > >
> > > Both Tested-by and Reviewed-by tags, once received on mailing list from tester
> > > or reviewer, should be added by author to the applicable patches when sending
> > > next versions. However if the patch has changed substantially in following
> > > version, these tags might not be applicable anymore and thus should be removed.
> > > Usually removal of someone's Tested-by or Reviewed-by tags should be mentioned
> > > in the patch changelog (after the '---' separator).
> > >
> > > Does this help you?
> >
> > Thanks so much, it does. My apologies to everyone whose reviewed-by tag I
> > failed to add :(
> >
> > I should have read that more document more carefully.
>
> No worries! The important part is your changes. The tags are easy
> to add. And now you know. ;-)
The first three of your patches could go in, but the last two require a
new herd7 release (for the lkmmv2 flag). Left to myself, I would hold
all five until we get a new herd7 release, but if it is important to
get the first three into the current merge window, please rebase them
to mainline some time this week. I would then send a pull request for
the for next week, the second and final week of the merge window.
Over to you!
Thanx, Paul
^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: [PATCH v4 5/5] tools/memory-model: Distinguish between syntactic and semantic tags
2024-11-18 15:05 ` Paul E. McKenney
@ 2024-11-26 15:25 ` Jonas Oberhauser
2024-11-26 16:03 ` Paul E. McKenney
0 siblings, 1 reply; 35+ messages in thread
From: Jonas Oberhauser @ 2024-11-26 15:25 UTC (permalink / raw)
To: paulmck
Cc: Akira Yokosawa, boqun.feng, dhowells, dlustig, frederic,
hernan.poncedeleon, j.alglave, joel, linux-kernel, lkmm,
luc.maranget, npiggin, parri.andrea, peterz, quic_neeraju, stern,
urezki, will
Am 11/18/2024 um 4:05 PM schrieb Paul E. McKenney:
> On Fri, Nov 08, 2024 at 10:35:24AM -0800, Paul E. McKenney wrote:
>>
>> And now you know. ;-)
>
> if it is important to
> get the first three into the current merge window, please rebase them
> to mainline some time this week
> Over to you!
Luckily there's no need and we can wait until a new herd release.
Have a lot of fun,
jonas
^ permalink raw reply [flat|nested] 35+ messages in thread
* Re: [PATCH v4 5/5] tools/memory-model: Distinguish between syntactic and semantic tags
2024-11-26 15:25 ` Jonas Oberhauser
@ 2024-11-26 16:03 ` Paul E. McKenney
0 siblings, 0 replies; 35+ messages in thread
From: Paul E. McKenney @ 2024-11-26 16:03 UTC (permalink / raw)
To: Jonas Oberhauser
Cc: Akira Yokosawa, boqun.feng, dhowells, dlustig, frederic,
hernan.poncedeleon, j.alglave, joel, linux-kernel, lkmm,
luc.maranget, npiggin, parri.andrea, peterz, quic_neeraju, stern,
urezki, will
On Tue, Nov 26, 2024 at 04:25:46PM +0100, Jonas Oberhauser wrote:
>
>
> Am 11/18/2024 um 4:05 PM schrieb Paul E. McKenney:
> > On Fri, Nov 08, 2024 at 10:35:24AM -0800, Paul E. McKenney wrote:
> >>
> > > And now you know. ;-)
> >
> > if it is important to
> > get the first three into the current merge window, please rebase them
> > to mainline some time this week
>
> > Over to you!
>
> Luckily there's no need and we can wait until a new herd release.
Sounds good, and here is hoping for sooner rather than later.
Thanx, Paul
^ permalink raw reply [flat|nested] 35+ messages in thread
end of thread, other threads:[~2024-11-26 16:03 UTC | newest]
Thread overview: 35+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2024-09-30 10:57 [PATCH v4 0/5] tools/memory-model: Define more of LKMM in tools/memory-model Jonas Oberhauser
2024-09-30 10:57 ` [PATCH v4 1/5] tools/memory-model: Legitimize current use of tags in LKMM macros Jonas Oberhauser
2024-10-28 22:11 ` Boqun Feng
2024-09-30 10:57 ` [PATCH v4 2/5] tools/memory-model: Define applicable tags on operation in tools/ Jonas Oberhauser
2024-10-28 22:12 ` Boqun Feng
2024-09-30 10:57 ` [PATCH v4 3/5] tools/memory-model: Define effect of Mb tags on RMWs " Jonas Oberhauser
2024-10-28 22:15 ` Boqun Feng
2024-09-30 10:57 ` [PATCH v4 4/5] tools/memory-model: Switch to softcoded herd7 tags Jonas Oberhauser
2024-10-02 17:34 ` Hernan Ponce de Leon
2024-10-29 0:04 ` Boqun Feng
2024-10-29 23:42 ` Paul E. McKenney
2024-10-30 11:50 ` Jonas Oberhauser
2024-10-30 13:46 ` Paul E. McKenney
2024-09-30 10:57 ` [PATCH v4 5/5] tools/memory-model: Distinguish between syntactic and semantic tags Jonas Oberhauser
2024-10-29 0:15 ` Boqun Feng
2024-10-29 23:41 ` Paul E. McKenney
2024-10-30 11:38 ` Jonas Oberhauser
2024-10-30 14:34 ` Boqun Feng
2024-10-30 16:27 ` Paul E. McKenney
2024-11-05 20:21 ` Paul E. McKenney
2024-11-06 10:28 ` Jonas Oberhauser
2024-11-06 15:04 ` Paul E. McKenney
2024-11-06 18:00 ` Paul E. McKenney
2024-11-07 9:05 ` Jonas Oberhauser
2024-11-07 10:51 ` Akira Yokosawa
2024-11-07 14:04 ` Paul E. McKenney
2024-11-08 9:10 ` Jonas Oberhauser
2024-11-08 10:12 ` Akira Yokosawa
2024-11-08 11:07 ` Jonas Oberhauser
2024-11-08 18:35 ` Paul E. McKenney
2024-11-18 15:05 ` Paul E. McKenney
2024-11-26 15:25 ` Jonas Oberhauser
2024-11-26 16:03 ` Paul E. McKenney
2024-10-28 20:16 ` [PATCH v4 0/5] tools/memory-model: Define more of LKMM in tools/memory-model Paul E. McKenney
2024-11-10 15:17 ` Akira Yokosawa
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®