[PATCHv2 0/4] tools/memory-model: Define more of LKMM in tools/memory-model

[PATCHv2 0/4] tools/memory-model: Define more of LKMM in tools/memory-model

[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 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

[PATCHv2 1/4] tools/memory-model: Legitimize current use of tags in LKMM macros

[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

[PATCHv2 2/4] tools/memory-model: Define applicable tags on operation in tools/...

[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 | 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

[PATCHv2 3/4] tools/memory-model: Define effect of Mb tags on RMWs in tools/...

[Jonas Oberhauser]

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

[PATCHv2 4/4] tools/memory-model: Distinguish between syntactic and semantic tags

[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  | 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

Re: [PATCHv2 0/4] tools/memory-model: Define more of LKMM in tools/memory-model

[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?

Alan

Re: [PATCHv2 2/4] tools/memory-model: Define applicable tags on operation in tools/...

[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 <jonas.oberhauser@huaweicloud.com>
> ---
>  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
> 

Re: [PATCHv2 3/4] tools/memory-model: Define effect of Mb tags on RMWs in tools/...

[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 <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]) |

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
> 

Re: [PATCHv2 2/4] tools/memory-model: Define applicable tags on operation in tools/...

[Jonas Oberhauser]

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 <jonas.oberhauser@huaweicloud.com>
>> ---
>>   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
>>

Re: [PATCHv2 3/4] tools/memory-model: Define effect of Mb tags on RMWs in tools/...

[Alan Stern]

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

Re: [PATCHv2 3/4] tools/memory-model: Define effect of Mb tags on RMWs in tools/...

[Jonas Oberhauser]

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 <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]) |
> 
> 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

Re: [PATCHv2 0/4] tools/memory-model: Define more of LKMM in tools/memory-model

[Jonas Oberhauser]

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.

Re: [PATCHv2 0/4] tools/memory-model: Define more of LKMM in tools/memory-model

[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.

							Thanx, Paul

Re: [PATCHv2 0/4] tools/memory-model: Define more of LKMM in tools/memory-model

[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.

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

Re: [PATCHv2 0/4] tools/memory-model: Define more of LKMM in tools/memory-model

[Jonas Oberhauser]

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

Re: [PATCHv2 0/4] tools/memory-model: Define more of LKMM in tools/memory-model

[Hernan Ponce de Leon]

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

Re: [PATCHv2 0/4] tools/memory-model: Define more of LKMM in tools/memory-model

[Jonas Oberhauser]

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

Re: [PATCHv2 0/4] tools/memory-model: Define more of LKMM in tools/memory-model

[Paul E. McKenney]

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

Re: [PATCHv2 3/4] tools/memory-model: Define effect of Mb tags on RMWs in tools/...

[Boqun Feng]

On Wed, Jun 05, 2024 at 09:56:31PM +0200, Jonas Oberhauser wrote:
> 
> 
> 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 <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]) |
> > 
> > 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.).
> 

May not be a good idea to model smp_store_mb() as a (Mb & W), since the
purpose of smp_store_mb() is for SB pattern synchronization. Maybe it
has a bad name, but I think the intentation of smp_store_mb() is simply
a write + smp_mb(), rather than a MB write.

Regards,
Boqun

> Best wishes,
>   jonas
> 

Re: [PATCHv2 0/4] tools/memory-model: Define more of LKMM in tools/memory-model

[Hernan Ponce de Leon]

On 6/10/2024 10:38 AM, Hernan Ponce de Leon wrote:
> 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

I pushed some new changes to the code for backward compatibility [1]. 
The series also needs the patch at the bottom to properly deal with the 
ordering of failing CAses and non-returning operations. With it, all 
litmus tests return the correct result (the script needs to pass option 
-lkmm-legacy false to herd).

Implementation-wise, there are two things that I would like to have:

- atomic_add_unless implementation is treated different than the rest 
and it is one of the few remaining cases where memory orderings are 
hardcoded [2]. I would like to define it in the .def file as

	atomic_add_unless(X,V,U) __atomic_add_unless{ONCE}(X,V,U)

- "deref" and "lderef" instructions seems to add a "rb_dep" fence. None 
of the model files (.cat, .def, .bell) refers to "rb_dep" so this looks 
useless to me. However, I never checked the details of these 
dereferencing instruction so I might be missing something. Maybe Paul 
can clarify.

Hernan

[1] https://github.com/herd/herdtools7/pull/865
[2] https://github.com/herd/herdtools7/issues/868


diff --git a/tools/memory-model/linux-kernel.def 
b/tools/memory-model/linux-kernel.def
index 001366ff3fb4..5a40c2cad39b 100644
--- a/tools/memory-model/linux-kernel.def
+++ b/tools/memory-model/linux-kernel.def
@@ -32,10 +32,10 @@ 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)
+cmpxchg(X,V,W) __cmpxchg{MB,ONCE}(X,V,W)
+cmpxchg_relaxed(X,V,W) __cmpxchg{ONCE,ONCE}(X,V,W)
+cmpxchg_acquire(X,V,W) __cmpxchg{ACQUIRE,ONCE}(X,V,W)
+cmpxchg_release(X,V,W) __cmpxchg{RELEASE,ONCE}(X,V,W)

  // Spinlocks
  spin_lock(X) { __lock(X); }
@@ -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)
@@ -127,10 +127,10 @@ 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_cmpxchg(X,V,W) __cmpxchg{MB,ONCE}(X,V,W)
+atomic_cmpxchg_relaxed(X,V,W) __cmpxchg{ONCE,ONCE}(X,V,W)
+atomic_cmpxchg_acquire(X,V,W) __cmpxchg{ACQUIRE,ONCE}(X,V,W)
+atomic_cmpxchg_release(X,V,W) __cmpxchg{RELEASE,ONCE}(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

Re: [PATCHv2 0/4] tools/memory-model: Define more of LKMM in tools/memory-model

[Hernan Ponce de Leon]

On 7/12/2024 10:06 AM, Hernan Ponce de Leon wrote:
> On 6/10/2024 10:38 AM, Hernan Ponce de Leon wrote:
>> 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
> 
> I pushed some new changes to the code for backward compatibility [1]. 
> The series also needs the patch at the bottom to properly deal with the 
> ordering of failing CAses and non-returning operations. With it, all 
> litmus tests return the correct result (the script needs to pass option 
> -lkmm-legacy false to herd).

I have been playing around with an alternative to this.

Rather than implementing this as an "option", I can implemented it as a 
"model variant (*)" and add this to the model

flag ~empty (if "lkmmlatest" then 0 else _)
   as new-lkmm-models-require-variant-lkmmlatest

If the user forgets to set the variant for the new model, herd7 will 
flag the executions showing that something is off.

To be fully backward compatible, we would need to backport this to old 
models

flag ~empty (if "lkmmlatest" then 1 else _)
   as new-lkmm-models-require-variant-lkmmlatest

If the user (wrongly) sets the variant for an old model, the the 
executions will be flagged.

Any thoughts?

Hernan

(*) This trick seems to be used for some arm models

https://github.com/herd/herdtools7/blob/master/herd/libdir/arm-models/mixed/ec.cat#L66C1-L67C67

> 
> Implementation-wise, there are two things that I would like to have:
> 
> - atomic_add_unless implementation is treated different than the rest 
> and it is one of the few remaining cases where memory orderings are 
> hardcoded [2]. I would like to define it in the .def file as
> 
>      atomic_add_unless(X,V,U) __atomic_add_unless{ONCE}(X,V,U)
> 
> - "deref" and "lderef" instructions seems to add a "rb_dep" fence. None 
> of the model files (.cat, .def, .bell) refers to "rb_dep" so this looks 
> useless to me. However, I never checked the details of these 
> dereferencing instruction so I might be missing something. Maybe Paul 
> can clarify.
> 
> Hernan
> 
> [1] https://github.com/herd/herdtools7/pull/865
> [2] https://github.com/herd/herdtools7/issues/868
> 
> 
> diff --git a/tools/memory-model/linux-kernel.def 
> b/tools/memory-model/linux-kernel.def
> index 001366ff3fb4..5a40c2cad39b 100644
> --- a/tools/memory-model/linux-kernel.def
> +++ b/tools/memory-model/linux-kernel.def
> @@ -32,10 +32,10 @@ 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)
> +cmpxchg(X,V,W) __cmpxchg{MB,ONCE}(X,V,W)
> +cmpxchg_relaxed(X,V,W) __cmpxchg{ONCE,ONCE}(X,V,W)
> +cmpxchg_acquire(X,V,W) __cmpxchg{ACQUIRE,ONCE}(X,V,W)
> +cmpxchg_release(X,V,W) __cmpxchg{RELEASE,ONCE}(X,V,W)
> 
>   // Spinlocks
>   spin_lock(X) { __lock(X); }
> @@ -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)
> @@ -127,10 +127,10 @@ 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_cmpxchg(X,V,W) __cmpxchg{MB,ONCE}(X,V,W)
> +atomic_cmpxchg_relaxed(X,V,W) __cmpxchg{ONCE,ONCE}(X,V,W)
> +atomic_cmpxchg_acquire(X,V,W) __cmpxchg{ACQUIRE,ONCE}(X,V,W)
> +atomic_cmpxchg_release(X,V,W) __cmpxchg{RELEASE,ONCE}(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

Re: [PATCHv2 0/4] tools/memory-model: Define more of LKMM in tools/memory-model

[Jonas Oberhauser]

Am 7/29/2024 um 3:30 PM schrieb Hernan Ponce de Leon:
> On 7/12/2024 10:06 AM, Hernan Ponce de Leon wrote:
>> On 6/10/2024 10:38 AM, Hernan Ponce de Leon wrote:
>>> 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
>>
>> I pushed some new changes to the code for backward compatibility [1]. 
>> The series also needs the patch at the bottom to properly deal with 
>> the ordering of failing CAses and non-returning operations. With it, 
>> all litmus tests return the correct result (the script needs to pass 
>> option -lkmm-legacy false to herd).
> 
> I have been playing around with an alternative to this.
> 
> Rather than implementing this as an "option", I can implemented it as a 
> "model variant (*)" and add this to the model

How exactly do these model variants get selected?

I was thinking that another good approach could be to have a new generic 
C model which doesn't know anything about LKMM. I believe this would be 
specified in the header of the .litmus files?


> flag ~empty (if "lkmmlatest" then 0 else _)
>    as new-lkmm-models-require-variant-lkmmlatest
> 
> If the user forgets to set the variant for the new model, herd7 will 
> flag the executions showing that something is off.
> 
> To be fully backward compatible, we would need to backport this to old 
> models
> 
> flag ~empty (if "lkmmlatest" then 1 else _)
>    as new-lkmm-models-require-variant-lkmmlatest

should this be then _ else 0  ? or what does the _ do here?

I also don't think we can backport things to old models

> If the user (wrongly) sets the variant for an old model, the the 
> executions will be flagged.
> 
> Any thoughts?
> 
> Hernan
> 
> (*) This trick seems to be used for some arm models
> 
> https://github.com/herd/herdtools7/blob/master/herd/libdir/arm-models/mixed/ec.cat#L66C1-L67C67

Re: [PATCHv2 0/4] tools/memory-model: Define more of LKMM in tools/memory-model

[Hernan Ponce de Leon]

On 7/29/2024 4:45 PM, Jonas Oberhauser wrote:
> 
> 
> Am 7/29/2024 um 3:30 PM schrieb Hernan Ponce de Leon:
>> On 7/12/2024 10:06 AM, Hernan Ponce de Leon wrote:
>>> On 6/10/2024 10:38 AM, Hernan Ponce de Leon wrote:
>>>> 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
>>>
>>> I pushed some new changes to the code for backward compatibility [1]. 
>>> The series also needs the patch at the bottom to properly deal with 
>>> the ordering of failing CAses and non-returning operations. With it, 
>>> all litmus tests return the correct result (the script needs to pass 
>>> option -lkmm-legacy false to herd).
>>
>> I have been playing around with an alternative to this.
>>
>> Rather than implementing this as an "option", I can implemented it as 
>> a "model variant (*)" and add this to the model
> 
> How exactly do these model variants get selected?
> 
> I was thinking that another good approach could be to have a new generic 
> C model which doesn't know anything about LKMM. I believe this would be 
> specified in the header of the .litmus files?
> 
> 
>> flag ~empty (if "lkmmlatest" then 0 else _)
>>    as new-lkmm-models-require-variant-lkmmlatest
>>
>> If the user forgets to set the variant for the new model, herd7 will 
>> flag the executions showing that something is off.
>>
>> To be fully backward compatible, we would need to backport this to old 
>> models
>>
>> flag ~empty (if "lkmmlatest" then 1 else _)
>>    as new-lkmm-models-require-variant-lkmmlatest
> 
> should this be then _ else 0  ? or what does the _ do here?

Yes, my bad.

> 
> I also don't think we can backport things to old models

IIRC I have seen (non lkmm related) patches being backported to stable 
kernel versions. Why can't we do this for lkmm if backward compatibility 
is really a requirement? Otherwise I don't see a way of preventing 
developers to use old models with the new option (since I plan to keep 
the "old variant" as default, this would have to be done on purpose, but 
still).

> 
>> If the user (wrongly) sets the variant for an old model, the the 
>> executions will be flagged.
>>
>> Any thoughts?
>>
>> Hernan
>>
>> (*) This trick seems to be used for some arm models
>>
>> https://github.com/herd/herdtools7/blob/master/herd/libdir/arm-models/mixed/ec.cat#L66C1-L67C67
> 

Re: [PATCHv2 0/4] tools/memory-model: Define more of LKMM in tools/memory-model

[Jonas Oberhauser]

Am 7/29/2024 um 5:19 PM schrieb Hernan Ponce de Leon:
> On 7/29/2024 4:45 PM, Jonas Oberhauser wrote:
>>
>>
>> Am 7/29/2024 um 3:30 PM schrieb Hernan Ponce de Leon:
>>> On 7/12/2024 10:06 AM, Hernan Ponce de Leon wrote:
>>>> On 6/10/2024 10:38 AM, Hernan Ponce de Leon wrote:
>>>>> 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
>>>>
>>>> I pushed some new changes to the code for backward compatibility 
>>>> [1]. The series also needs the patch at the bottom to properly deal 
>>>> with the ordering of failing CAses and non-returning operations. 
>>>> With it, all litmus tests return the correct result (the script 
>>>> needs to pass option -lkmm-legacy false to herd).
>>>
>>> I have been playing around with an alternative to this.
>>>
>>> Rather than implementing this as an "option", I can implemented it as 
>>> a "model variant (*)" and add this to the model
>>
>> How exactly do these model variants get selected?
>>
>> I was thinking that another good approach could be to have a new 
>> generic C model which doesn't know anything about LKMM. I believe this 
>> would be specified in the header of the .litmus files?
>>
>>
>>> flag ~empty (if "lkmmlatest" then 0 else _)
>>>    as new-lkmm-models-require-variant-lkmmlatest
>>>
>>> If the user forgets to set the variant for the new model, herd7 will 
>>> flag the executions showing that something is off.
>>>
>>> To be fully backward compatible, we would need to backport this to 
>>> old models
>>>
>>> flag ~empty (if "lkmmlatest" then 1 else _)
>>>    as new-lkmm-models-require-variant-lkmmlatest
>>
>> should this be then _ else 0  ? or what does the _ do here?
> 
> Yes, my bad.
> 
>>
>> I also don't think we can backport things to old models
> 
> IIRC I have seen (non lkmm related) patches being backported to stable 
> kernel versions. Why can't we do this for lkmm if backward compatibility 
> is really a requirement? Otherwise I don't see a way of preventing 
> developers to use old models with the new option (since I plan to keep 
> the "old variant" as default, this would have to be done on purpose, but 
> still).

I don't think this is a problem. If the old version is the default, and 
we define it in the .cfg file for the tree version of LKMM, then it will 
work correctly for both the old and new versions. People playing around 
with Memory Models should be careful enough not to intentionally break 
the model by passing bogus options.

Of course, defining a new syntax identifier and putting it in all 
headers would be more robust. But it's more work and I would only do 
that if we really got rid of all the LKMM specifics.

Have fun,
   jonas

Re: [PATCHv2 0/4] tools/memory-model: Define more of LKMM in tools/memory-model

[Hernan Ponce de Leon]

On 7/29/2024 5:44 PM, Jonas Oberhauser wrote:
> 
> 
> Am 7/29/2024 um 5:19 PM schrieb Hernan Ponce de Leon:
>> On 7/29/2024 4:45 PM, Jonas Oberhauser wrote:
>>>
>>>
>>> Am 7/29/2024 um 3:30 PM schrieb Hernan Ponce de Leon:
>>>> On 7/12/2024 10:06 AM, Hernan Ponce de Leon wrote:
>>>>> On 6/10/2024 10:38 AM, Hernan Ponce de Leon wrote:
>>>>>> 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
>>>>>
>>>>> I pushed some new changes to the code for backward compatibility 
>>>>> [1]. The series also needs the patch at the bottom to properly deal 
>>>>> with the ordering of failing CAses and non-returning operations. 
>>>>> With it, all litmus tests return the correct result (the script 
>>>>> needs to pass option -lkmm-legacy false to herd).
>>>>
>>>> I have been playing around with an alternative to this.
>>>>
>>>> Rather than implementing this as an "option", I can implemented it 
>>>> as a "model variant (*)" and add this to the model
>>>
>>> How exactly do these model variants get selected?
>>>
>>> I was thinking that another good approach could be to have a new 
>>> generic C model which doesn't know anything about LKMM. I believe 
>>> this would be specified in the header of the .litmus files?
>>>
>>>
>>>> flag ~empty (if "lkmmlatest" then 0 else _)
>>>>    as new-lkmm-models-require-variant-lkmmlatest
>>>>
>>>> If the user forgets to set the variant for the new model, herd7 will 
>>>> flag the executions showing that something is off.
>>>>
>>>> To be fully backward compatible, we would need to backport this to 
>>>> old models
>>>>
>>>> flag ~empty (if "lkmmlatest" then 1 else _)
>>>>    as new-lkmm-models-require-variant-lkmmlatest
>>>
>>> should this be then _ else 0  ? or what does the _ do here?
>>
>> Yes, my bad.
>>
>>>
>>> I also don't think we can backport things to old models
>>
>> IIRC I have seen (non lkmm related) patches being backported to stable 
>> kernel versions. Why can't we do this for lkmm if backward 
>> compatibility is really a requirement? Otherwise I don't see a way of 
>> preventing developers to use old models with the new option (since I 
>> plan to keep the "old variant" as default, this would have to be done 
>> on purpose, but still).
> 
> I don't think this is a problem. If the old version is the default, and 
> we define it in the .cfg file for the tree version of LKMM, then it will 
> work correctly for both the old and new versions. People playing around 
> with Memory Models should be careful enough not to intentionally break 
> the model by passing bogus options.

The same was true for my implementation using the lkmm-legacy option 
rather than the model variant, but this was still considered to break 
backward compatibility.

https://github.com/herd/herdtools7/pull/865#issuecomment-2229930493

> 
> Of course, defining a new syntax identifier and putting it in all 
> headers would be more robust. But it's more work and I would only do 
> that if we really got rid of all the LKMM specifics.
> 
> Have fun,
>    jonas

Re: [PATCHv2 0/4] tools/memory-model: Define more of LKMM in tools/memory-model

[Jonas Oberhauser]

Am 7/29/2024 um 5:53 PM schrieb Hernan Ponce de Leon:
> On 7/29/2024 5:44 PM, Jonas Oberhauser wrote:
>>
>>
>> I don't think this is a problem. If the old version is the default, 
>> and we define it in the .cfg file for the tree version of LKMM, then 
>> it will work correctly for both the old and new versions. People 
>> playing around with Memory Models should be careful enough not to 
>> intentionally break the model by passing bogus options.
> 
> The same was true for my implementation using the lkmm-legacy option

Yeah, I'm fine with that one. (Although it may be better to have a 
version number as value instead of just a boolean flag, like 
-model-version=x_y_z - just in case this is not the last time).

> rather than the model variant, but this was still considered to break 
> backward compatibility.
> 
> https://github.com/herd/herdtools7/pull/865#issuecomment-2229930493

I think Akira is a bit overzealous here. What if a user accidentally 
puts -lkmm-legacy false and accidentally also adds the version number 
into the litmus test and/or model?

The request can be fulfilled, by defining some relation in the bell file 
that has a magic name like version_x_y_z and checks that the x_y_z 
matches the -model-version=x_y_z provided as an argument.

But I don't think we need to go that far.

jonas