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 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 since v1:
- addressed several spelling/style issues pointed out by Alan
- simplified the definition of Marked accesses based on a
suggestion by Alan
Jonas Oberhauser (4):
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: Distinguish between syntactic and semantic tags
tools/memory-model/linux-kernel.bell | 26 ++--
tools/memory-model/linux-kernel.cat | 10 ++
tools/memory-model/linux-kernel.def | 176 +++++++++++++--------------
3 files changed, 115 insertions(+), 97 deletions(-)
--
2.34.1
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 <[email protected]>
---
tools/memory-model/linux-kernel.bell | 7 +++++++
1 file changed, 7 insertions(+)
diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
index dba6b5b6dee0..2f49993644ed 100644
--- a/tools/memory-model/linux-kernel.bell
+++ b/tools/memory-model/linux-kernel.bell
@@ -36,6 +36,13 @@ enum Barriers = 'wmb (*smp_wmb*) ||
'after-srcu-read-unlock (*smp_mb__after_srcu_read_unlock*)
instructions F[Barriers]
+(* Remove impossible tags, such as Acquire on a store or 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
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 <[email protected]>
Suggested-by: Alan Stern <[email protected]>
Signed-off-by: Jonas Oberhauser <[email protected]>
---
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
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 <[email protected]>
---
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
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 <[email protected]>
Signed-off-by: Jonas Oberhauser <[email protected]>
---
tools/memory-model/linux-kernel.bell | 22 ++--
tools/memory-model/linux-kernel.def | 176 +++++++++++++--------------
2 files changed, 99 insertions(+), 99 deletions(-)
diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
index 2f49993644ed..a27757470d29 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*) ||
@@ -38,10 +38,10 @@ instructions F[Barriers]
(* Remove impossible tags, such as Acquire on a store or 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
@@ -81,7 +81,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 a12b96c547b7..001366ff3fb4 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); }
@@ -72,75 +72,75 @@ atomic_inc(X) { __atomic_op(X,+,1); }
atomic_dec(X) { __atomic_op(X,-,1); }
atomic_andnot(V,X) { __atomic_op(X,&~,V); }
-atomic_add_return(V,X) __atomic_op_return{mb}(X,+,V)
-atomic_add_return_relaxed(V,X) __atomic_op_return{once}(X,+,V)
-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_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)
--
2.34.1
On Tue, Jun 04, 2024 at 05:29:18PM +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 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.
The patches look good to me.
Just to clarify: Your first step encompasses patches 1 - 3, and the
second step is patch 4. The first three patches can be applied now, but
the last one needs to wait until herd7 has been updated. Is this all
correct?
Alan
On Tue, Jun 04, 2024 at 06:04:09PM +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 <[email protected]>
> ---
> tools/memory-model/linux-kernel.bell | 7 +++++++
> 1 file changed, 7 insertions(+)
>
> diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
> index dba6b5b6dee0..2f49993644ed 100644
> --- a/tools/memory-model/linux-kernel.bell
> +++ b/tools/memory-model/linux-kernel.bell
> @@ -36,6 +36,13 @@ enum Barriers = 'wmb (*smp_wmb*) ||
> 'after-srcu-read-unlock (*smp_mb__after_srcu_read_unlock*)
> instructions F[Barriers]
>
> +(* Remove impossible tags, such as Acquire on a store or failed RMW *)
This comment needs a bit help, "failed RMW"s still exist, they just
don't provide ordering. How about:
(*
* Filter out syntactic annotations that don't provide the corresponding
* semantic ordering, such as Acquire on a store or Mb on a failed RMW.
*)
?
Regards,
Boqun
> +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
>
On Tue, Jun 04, 2024 at 06:04:40PM +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 <[email protected]>
> Suggested-by: Alan Stern <[email protected]>
> Signed-off-by: Jonas Oberhauser <[email protected]>
> ---
> 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]) |
I couldn't help suggestting:
([M] ; po ; [Mb & domain(rmw)]) |
([Mb & range(rmw)] ; po ; [M]) |
, it's a bit more clear to me, but maybe the comment above is good
enough?
Regards,
Boqun
> ([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) |
> ([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) |
> ([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) |
> --
> 2.34.1
>
Am 6/5/2024 um 6:25 AM schrieb Boqun Feng:
> On Tue, Jun 04, 2024 at 06:04:09PM +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 <[email protected]>
>> ---
>> tools/memory-model/linux-kernel.bell | 7 +++++++
>> 1 file changed, 7 insertions(+)
>>
>> diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
>> index dba6b5b6dee0..2f49993644ed 100644
>> --- a/tools/memory-model/linux-kernel.bell
>> +++ b/tools/memory-model/linux-kernel.bell
>> @@ -36,6 +36,13 @@ enum Barriers = 'wmb (*smp_wmb*) ||
>> 'after-srcu-read-unlock (*smp_mb__after_srcu_read_unlock*)
>> instructions F[Barriers]
>>
>> +(* Remove impossible tags, such as Acquire on a store or failed RMW *)
>
> This comment needs a bit help, "failed RMW"s still exist, they just
> don't provide ordering. How about:
Oh, I see how the comment can be misread. A smaller fix would be
"Acquire on a store or on a failed RMW"
but I actually like your longer explanation better, so I think I'll go
with that.
>
> (*
> * Filter out syntactic annotations that don't provide the corresponding
> * semantic ordering, such as Acquire on a store or Mb on a failed RMW.
> *)
>
> ?
>
> Regards,
> Boqun
>
>> +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
>>
On Tue, Jun 04, 2024 at 09:28:42PM -0700, Boqun Feng wrote:
> On Tue, Jun 04, 2024 at 06:04:40PM +0200, Jonas Oberhauser wrote:
> > --- 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]) |
>
> I couldn't help suggestting:
>
> ([M] ; po ; [Mb & domain(rmw)]) |
> ([Mb & range(rmw)] ; po ; [M]) |
>
> , it's a bit more clear to me, but maybe the comment above is good
> enough?
We may want to use the patch's approach for other things besides RMW.
For instance, it would be a good way to implement smp_store_mb() --
compare it to the existing implementation in the .def file.
Alan
Am 6/5/2024 um 6:28 AM schrieb Boqun Feng:
> On Tue, Jun 04, 2024 at 06:04:40PM +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 <[email protected]>
>> Suggested-by: Alan Stern <[email protected]>
>> Signed-off-by: Jonas Oberhauser <[email protected]>
>> ---
>> 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]) |
>
> I couldn't help suggestting:
>
> ([M] ; po ; [Mb & domain(rmw)]) |
> ([Mb & range(rmw)] ; po ; [M]) |
>
> , it's a bit more clear to me, but maybe the comment above is good
> enough?
Hm, maybe clarity is in the eye of the beholder in this case.
Actually looking at your suggestion makes me think of smp_store_mb(),
which although represented as Once;F[Mb] could be (mis)understood also
as Mb&W. And it indeed does the same thing
([Mb & W] ; po ; [M])
would suggest.
(btw I think it is confusing that smp_store_mb is not strictly stronger
than smp_store_release. Of course there are places where you want a
relaxed store followed by an mb, but usually the mb versions are
strictly stronger.).
Best wishes,
jonas
Am 6/4/2024 um 7:56 PM schrieb Alan Stern:
> On Tue, Jun 04, 2024 at 05:29:18PM +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 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.
>
> The patches look good to me.
>
> Just to clarify: Your first step encompasses patches 1 - 3, and the
> second step is patch 4. The first three patches can be applied now, but
> the last one needs to wait until herd7 has been updated. Is this all
> correct?
Exactly.
On Wed, Jun 05, 2024 at 09:58:42PM +0200, Jonas Oberhauser wrote:
>
>
> Am 6/4/2024 um 7:56 PM schrieb Alan Stern:
> > On Tue, Jun 04, 2024 at 05:29:18PM +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 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.
> >
> > The patches look good to me.
> >
> > Just to clarify: Your first step encompasses patches 1 - 3, and the
> > second step is patch 4. The first three patches can be applied now, but
> > the last one needs to wait until herd7 has been updated. Is this all
> > correct?
>
> Exactly.
Just to make sure that I am following along properly... My belief is
that there will be a new version of this series. Please let me know if
I am missing something.
Thanx, Paul
On Wed, Jun 05, 2024 at 09:58:42PM +0200, Jonas Oberhauser wrote:
>
>
> Am 6/4/2024 um 7:56 PM schrieb Alan Stern:
> > Just to clarify: Your first step encompasses patches 1 - 3, and the
> > second step is patch 4. The first three patches can be applied now, but
> > the last one needs to wait until herd7 has been updated. Is this all
> > correct?
>
> Exactly.
With regard to patch 4, how much thought have you and Hernan given to
backward compatibility? Once herd7 is changed, old memory model files
will no longer work correctly.
To avoid being so disruptive, perhaps the changes to herd7 should be
under control of a new command-line or config-file switch. If the
switch is enabled, the new simplified code gets used; otherwise herd7
would continue to use its old built-in rules for special tags.
Alan
Am 6/6/2024 um 6:37 PM schrieb Paul E. McKenney:
> On Wed, Jun 05, 2024 at 09:58:42PM +0200, Jonas Oberhauser wrote:
>>
>>
>> Am 6/4/2024 um 7:56 PM schrieb Alan Stern:
>>> On Tue, Jun 04, 2024 at 05:29:18PM +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 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.
>>>
>>> The patches look good to me.
>>>
>>> Just to clarify: Your first step encompasses patches 1 - 3, and the
>>> second step is patch 4. The first three patches can be applied now, but
>>> the last one needs to wait until herd7 has been updated. Is this all
>>> correct?
>>
>> Exactly.
>
> Just to make sure that I am following along properly... My belief is
> that there will be a new version of this series. Please let me know if
> I am missing something.
At least one :))
Have fun,
jonas
On 6/8/2024 3:00 AM, Alan Stern wrote:
> On Wed, Jun 05, 2024 at 09:58:42PM +0200, Jonas Oberhauser wrote:
>>
>>
>> Am 6/4/2024 um 7:56 PM schrieb Alan Stern:
>>> Just to clarify: Your first step encompasses patches 1 - 3, and the
>>> second step is patch 4. The first three patches can be applied now, but
>>> the last one needs to wait until herd7 has been updated. Is this all
>>> correct?
>>
>> Exactly.
>
> With regard to patch 4, how much thought have you and Hernan given to
> backward compatibility? Once herd7 is changed, old memory model files
> will no longer work correctly.
>
Honestly, I did not think much about this (at least until Akira
mentioned in my PR). My hope was that changes to the model could be
back-ported to previous kernel versions. However that would not work for
existing out-of-tree files.
My question is: is compatibility with out-of-tree files really a
requirement? I would argue that if people are using outdated models,
they may get wrong results anyway. This is because some of the changes
done to lkmm during the last few years change the expected result for
some litmus tests.
Hernan
Am 6/8/2024 um 3:00 AM schrieb Alan Stern:
> On Wed, Jun 05, 2024 at 09:58:42PM +0200, Jonas Oberhauser wrote:
>>
>>
>> Am 6/4/2024 um 7:56 PM schrieb Alan Stern:
>>> Just to clarify: Your first step encompasses patches 1 - 3, and the
>>> second step is patch 4. The first three patches can be applied now, but
>>> the last one needs to wait until herd7 has been updated. Is this all
>>> correct?
>>
>> Exactly.
>
> With regard to patch 4, how much thought have you and Hernan given to
> backward compatibility? Once herd7 is changed, old memory model files
> will no longer work correctly.
Yes, Akira pointed this out too.
My thought back then was to update herd now, and wait with the fourth
patch for a while until most people who run the LKMM would have
upgraded. However...
> To avoid being so disruptive, perhaps the changes to herd7 should be
> under control of a new command-line or config-file switch. If the
> switch is enabled, the new simplified code gets used; otherwise herd7
> would continue to use its old built-in rules for special tags
... I like that idea a lot better actually. I think it needs to be
placed into the files, or people will get strange, silent results.
But then I think we need to make sure that there's no internal behaviors
left. I don't want to introduce more flags in the future to turn off
other internal behavior.
jonas
On Mon, Jun 10, 2024 at 10:04:26AM +0200, Jonas Oberhauser wrote:
>
>
> Am 6/6/2024 um 6:37 PM schrieb Paul E. McKenney:
> > On Wed, Jun 05, 2024 at 09:58:42PM +0200, Jonas Oberhauser wrote:
> > >
> > >
> > > Am 6/4/2024 um 7:56 PM schrieb Alan Stern:
> > > > On Tue, Jun 04, 2024 at 05:29:18PM +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 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.
> > > >
> > > > The patches look good to me.
> > > >
> > > > Just to clarify: Your first step encompasses patches 1 - 3, and the
> > > > second step is patch 4. The first three patches can be applied now, but
> > > > the last one needs to wait until herd7 has been updated. Is this all
> > > > correct?
> > >
> > > Exactly.
> >
> > Just to make sure that I am following along properly... My belief is
> > that there will be a new version of this series. Please let me know if
> > I am missing something.
>
> At least one :))
;-) ;-) ;-)
I will await a later version, then.
Thanx, Paul