A new version of herd7 provides a -lkmmv2 switch which overrides the old herd7
behavior of simply ignoring any softcoded tags in the .def and .bell files. We
port LKMM to this version of herd7 by providing the switch in linux-kernel.cfg
and reporting an error if the LKMM is used without this switch.
To preserve the semantics of LKMM, we also softcode the Noreturn tag on atomic
RMW which do not return a value and define atomic_add_unless with an Mb tag in
linux-kernel.def.
We update the herd-representation.txt accordingly and clarify some of the
resulting combinations.
(To be) Signed-off-by: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>
Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
---
.../Documentation/herd-representation.txt | 27 ++++++++++---------
tools/memory-model/README | 2 +-
tools/memory-model/linux-kernel.bell | 3 +++
tools/memory-model/linux-kernel.cfg | 1 +
tools/memory-model/linux-kernel.def | 18 +++++++------
5 files changed, 30 insertions(+), 21 deletions(-)
diff --git a/tools/memory-model/Documentation/herd-representation.txt b/tools/memory-model/Documentation/herd-representation.txt
index ed988906f2b7..7ae1ff3d3769 100644
--- a/tools/memory-model/Documentation/herd-representation.txt
+++ b/tools/memory-model/Documentation/herd-representation.txt
@@ -18,6 +18,11 @@
#
# By convention, a blank line in a cell means "same as the preceding line".
#
+# Note that the syntactic representation does not always match the sets and
+# relations in linux-kernel.cat, due to redefinitions in linux-kernel.bell and
+# lock.cat. For example, the po link between LKR and LKW is upgraded to an rmw
+# link, and W[acquire] are not included in the Acquire set.
+#
# Disclaimer. The table includes representations of "add" and "and" operations;
# corresponding/identical representations of "sub", "inc", "dec" and "or", "xor",
# "andnot" operations are omitted.
@@ -60,14 +65,13 @@
------------------------------------------------------------------------------
| RMW ops w/o return value | |
------------------------------------------------------------------------------
- | atomic_add | R*[noreturn] ->rmw W*[once] |
+ | atomic_add | R*[noreturn] ->rmw W*[noreturn] |
| atomic_and | |
| spin_lock | LKR ->po LKW |
------------------------------------------------------------------------------
| RMW ops w/ return value | |
------------------------------------------------------------------------------
- | atomic_add_return | F[mb] ->po R*[once] |
- | | ->rmw W*[once] ->po F[mb] |
+ | atomic_add_return | R*[mb] ->rmw W*[mb] |
| atomic_fetch_add | |
| atomic_fetch_and | |
| atomic_xchg | |
@@ -79,13 +83,13 @@
| atomic_xchg_relaxed | |
| xchg_relaxed | |
| atomic_add_negative_relaxed | |
- | atomic_add_return_acquire | R*[acquire] ->rmw W*[once] |
+ | atomic_add_return_acquire | R*[acquire] ->rmw W*[acquire] |
| atomic_fetch_add_acquire | |
| atomic_fetch_and_acquire | |
| atomic_xchg_acquire | |
| xchg_acquire | |
| atomic_add_negative_acquire | |
- | atomic_add_return_release | R*[once] ->rmw W*[release] |
+ | atomic_add_return_release | R*[release] ->rmw W*[release] |
| atomic_fetch_add_release | |
| atomic_fetch_and_release | |
| atomic_xchg_release | |
@@ -94,17 +98,16 @@
------------------------------------------------------------------------------
| Conditional RMW ops | |
------------------------------------------------------------------------------
- | atomic_cmpxchg | On success: F[mb] ->po R*[once] |
- | | ->rmw W*[once] ->po F[mb] |
- | | On failure: R*[once] |
+ | atomic_cmpxchg | On success: R*[mb] ->rmw W*[mb] |
+ | | On failure: R*[mb] |
| cmpxchg | |
| atomic_add_unless | |
| atomic_cmpxchg_relaxed | On success: R*[once] ->rmw W*[once] |
| | On failure: R*[once] |
- | atomic_cmpxchg_acquire | On success: R*[acquire] ->rmw W*[once] |
- | | On failure: R*[once] |
- | atomic_cmpxchg_release | On success: R*[once] ->rmw W*[release] |
- | | On failure: R*[once] |
+ | atomic_cmpxchg_acquire | On success: R*[acquire] ->rmw W*[acquire] |
+ | | On failure: R*[acquire] |
+ | atomic_cmpxchg_release | On success: R*[release] ->rmw W*[release] |
+ | | On failure: R*[release] |
| spin_trylock | On success: LKR ->po LKW |
| | On failure: LF |
------------------------------------------------------------------------------
diff --git a/tools/memory-model/README b/tools/memory-model/README
index dab38904206a..59bc15edeb8a 100644
--- a/tools/memory-model/README
+++ b/tools/memory-model/README
@@ -20,7 +20,7 @@ that litmus test to be exercised within the Linux kernel.
REQUIREMENTS
============
-Version 7.52 or higher of the "herd7" and "klitmus7" tools must be
+Version 7.58 or higher of the "herd7" and "klitmus7" tools must be
downloaded separately:
https://github.com/herd/herdtools7
diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
index 7c9ae48b9437..8ae47545df97 100644
--- a/tools/memory-model/linux-kernel.bell
+++ b/tools/memory-model/linux-kernel.bell
@@ -94,3 +94,6 @@ let carry-dep = (data ; [~ Srcu-unlock] ; rfi)*
let addr = carry-dep ; addr
let ctrl = carry-dep ; ctrl
let data = carry-dep ; data
+
+flag ~empty (if "lkmmv2" then 0 else _)
+ as this-model-requires-variant-higher-than-lkmmv1
diff --git a/tools/memory-model/linux-kernel.cfg b/tools/memory-model/linux-kernel.cfg
index 3c8098e99f41..69b04f3aad73 100644
--- a/tools/memory-model/linux-kernel.cfg
+++ b/tools/memory-model/linux-kernel.cfg
@@ -1,6 +1,7 @@
macros linux-kernel.def
bell linux-kernel.bell
model linux-kernel.cat
+variant lkmmv2
graph columns
squished true
showevents noregs
diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
index a12b96c547b7..d7279a357cba 100644
--- a/tools/memory-model/linux-kernel.def
+++ b/tools/memory-model/linux-kernel.def
@@ -63,14 +63,14 @@ atomic_set(X,V) { WRITE_ONCE(*X,V); }
atomic_read_acquire(X) smp_load_acquire(X)
atomic_set_release(X,V) { smp_store_release(X,V); }
-atomic_add(V,X) { __atomic_op(X,+,V); }
-atomic_sub(V,X) { __atomic_op(X,-,V); }
-atomic_and(V,X) { __atomic_op(X,&,V); }
-atomic_or(V,X) { __atomic_op(X,|,V); }
-atomic_xor(V,X) { __atomic_op(X,^,V); }
-atomic_inc(X) { __atomic_op(X,+,1); }
-atomic_dec(X) { __atomic_op(X,-,1); }
-atomic_andnot(V,X) { __atomic_op(X,&~,V); }
+atomic_add(V,X) { __atomic_op{noreturn}(X,+,V); }
+atomic_sub(V,X) { __atomic_op{noreturn}(X,-,V); }
+atomic_and(V,X) { __atomic_op{noreturn}(X,&,V); }
+atomic_or(V,X) { __atomic_op{noreturn}(X,|,V); }
+atomic_xor(V,X) { __atomic_op{noreturn}(X,^,V); }
+atomic_inc(X) { __atomic_op{noreturn}(X,+,1); }
+atomic_dec(X) { __atomic_op{noreturn}(X,-,1); }
+atomic_andnot(V,X) { __atomic_op{noreturn}(X,&~,V); }
atomic_add_return(V,X) __atomic_op_return{mb}(X,+,V)
atomic_add_return_relaxed(V,X) __atomic_op_return{once}(X,+,V)
@@ -144,3 +144,5 @@ atomic_fetch_andnot(V,X) __atomic_fetch_op{mb}(X,&~,V)
atomic_fetch_andnot_acquire(V,X) __atomic_fetch_op{acquire}(X,&~,V)
atomic_fetch_andnot_release(V,X) __atomic_fetch_op{release}(X,&~,V)
atomic_fetch_andnot_relaxed(V,X) __atomic_fetch_op{once}(X,&~,V)
+
+atomic_add_unless(X,V,W) __atomic_add_unless{mb}(X,V,W)
--
2.34.1On Mon, Sep 30, 2024 at 12:57:09PM +0200, Jonas Oberhauser wrote:
> A new version of herd7 provides a -lkmmv2 switch which overrides the old herd7
> behavior of simply ignoring any softcoded tags in the .def and .bell files. We
> port LKMM to this version of herd7 by providing the switch in linux-kernel.cfg
> and reporting an error if the LKMM is used without this switch.
>
> To preserve the semantics of LKMM, we also softcode the Noreturn tag on atomic
> RMW which do not return a value and define atomic_add_unless with an Mb tag in
> linux-kernel.def.
>
> We update the herd-representation.txt accordingly and clarify some of the
> resulting combinations.
>
> (To be) Signed-off-by: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>
> Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
One bit below:
> ---
> .../Documentation/herd-representation.txt | 27 ++++++++++---------
> tools/memory-model/README | 2 +-
> tools/memory-model/linux-kernel.bell | 3 +++
> tools/memory-model/linux-kernel.cfg | 1 +
> tools/memory-model/linux-kernel.def | 18 +++++++------
> 5 files changed, 30 insertions(+), 21 deletions(-)
>
> diff --git a/tools/memory-model/Documentation/herd-representation.txt b/tools/memory-model/Documentation/herd-representation.txt
> index ed988906f2b7..7ae1ff3d3769 100644
> --- a/tools/memory-model/Documentation/herd-representation.txt
> +++ b/tools/memory-model/Documentation/herd-representation.txt
> @@ -18,6 +18,11 @@
> #
> # By convention, a blank line in a cell means "same as the preceding line".
> #
> +# Note that the syntactic representation does not always match the sets and
> +# relations in linux-kernel.cat, due to redefinitions in linux-kernel.bell and
> +# lock.cat. For example, the po link between LKR and LKW is upgraded to an rmw
> +# link, and W[acquire] are not included in the Acquire set.
> +#
> # Disclaimer. The table includes representations of "add" and "and" operations;
> # corresponding/identical representations of "sub", "inc", "dec" and "or", "xor",
> # "andnot" operations are omitted.
> @@ -60,14 +65,13 @@
> ------------------------------------------------------------------------------
> | RMW ops w/o return value | |
> ------------------------------------------------------------------------------
> - | atomic_add | R*[noreturn] ->rmw W*[once] |
> + | atomic_add | R*[noreturn] ->rmw W*[noreturn] |
Not in this patch, but don't you need to update this again to all cap
to match your changes in patch #5? ;-)
Regards,
Boqun
> | atomic_and | |
> | spin_lock | LKR ->po LKW |
> ------------------------------------------------------------------------------
> | RMW ops w/ return value | |
> ------------------------------------------------------------------------------
> - | atomic_add_return | F[mb] ->po R*[once] |
> - | | ->rmw W*[once] ->po F[mb] |
> + | atomic_add_return | R*[mb] ->rmw W*[mb] |
> | atomic_fetch_add | |
> | atomic_fetch_and | |
> | atomic_xchg | |
> @@ -79,13 +83,13 @@
> | atomic_xchg_relaxed | |
> | xchg_relaxed | |
> | atomic_add_negative_relaxed | |
> - | atomic_add_return_acquire | R*[acquire] ->rmw W*[once] |
> + | atomic_add_return_acquire | R*[acquire] ->rmw W*[acquire] |
> | atomic_fetch_add_acquire | |
> | atomic_fetch_and_acquire | |
> | atomic_xchg_acquire | |
> | xchg_acquire | |
> | atomic_add_negative_acquire | |
> - | atomic_add_return_release | R*[once] ->rmw W*[release] |
> + | atomic_add_return_release | R*[release] ->rmw W*[release] |
> | atomic_fetch_add_release | |
> | atomic_fetch_and_release | |
> | atomic_xchg_release | |
> @@ -94,17 +98,16 @@
> ------------------------------------------------------------------------------
> | Conditional RMW ops | |
> ------------------------------------------------------------------------------
> - | atomic_cmpxchg | On success: F[mb] ->po R*[once] |
> - | | ->rmw W*[once] ->po F[mb] |
> - | | On failure: R*[once] |
> + | atomic_cmpxchg | On success: R*[mb] ->rmw W*[mb] |
> + | | On failure: R*[mb] |
> | cmpxchg | |
> | atomic_add_unless | |
> | atomic_cmpxchg_relaxed | On success: R*[once] ->rmw W*[once] |
> | | On failure: R*[once] |
> - | atomic_cmpxchg_acquire | On success: R*[acquire] ->rmw W*[once] |
> - | | On failure: R*[once] |
> - | atomic_cmpxchg_release | On success: R*[once] ->rmw W*[release] |
> - | | On failure: R*[once] |
> + | atomic_cmpxchg_acquire | On success: R*[acquire] ->rmw W*[acquire] |
> + | | On failure: R*[acquire] |
> + | atomic_cmpxchg_release | On success: R*[release] ->rmw W*[release] |
> + | | On failure: R*[release] |
> | spin_trylock | On success: LKR ->po LKW |
> | | On failure: LF |
> ------------------------------------------------------------------------------
> diff --git a/tools/memory-model/README b/tools/memory-model/README
> index dab38904206a..59bc15edeb8a 100644
> --- a/tools/memory-model/README
> +++ b/tools/memory-model/README
> @@ -20,7 +20,7 @@ that litmus test to be exercised within the Linux kernel.
> REQUIREMENTS
> ============
>
> -Version 7.52 or higher of the "herd7" and "klitmus7" tools must be
> +Version 7.58 or higher of the "herd7" and "klitmus7" tools must be
> downloaded separately:
>
> https://github.com/herd/herdtools7
> diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
> index 7c9ae48b9437..8ae47545df97 100644
> --- a/tools/memory-model/linux-kernel.bell
> +++ b/tools/memory-model/linux-kernel.bell
> @@ -94,3 +94,6 @@ let carry-dep = (data ; [~ Srcu-unlock] ; rfi)*
> let addr = carry-dep ; addr
> let ctrl = carry-dep ; ctrl
> let data = carry-dep ; data
> +
> +flag ~empty (if "lkmmv2" then 0 else _)
> + as this-model-requires-variant-higher-than-lkmmv1
> diff --git a/tools/memory-model/linux-kernel.cfg b/tools/memory-model/linux-kernel.cfg
> index 3c8098e99f41..69b04f3aad73 100644
> --- a/tools/memory-model/linux-kernel.cfg
> +++ b/tools/memory-model/linux-kernel.cfg
> @@ -1,6 +1,7 @@
> macros linux-kernel.def
> bell linux-kernel.bell
> model linux-kernel.cat
> +variant lkmmv2
> graph columns
> squished true
> showevents noregs
> diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
> index a12b96c547b7..d7279a357cba 100644
> --- a/tools/memory-model/linux-kernel.def
> +++ b/tools/memory-model/linux-kernel.def
> @@ -63,14 +63,14 @@ atomic_set(X,V) { WRITE_ONCE(*X,V); }
> atomic_read_acquire(X) smp_load_acquire(X)
> atomic_set_release(X,V) { smp_store_release(X,V); }
>
> -atomic_add(V,X) { __atomic_op(X,+,V); }
> -atomic_sub(V,X) { __atomic_op(X,-,V); }
> -atomic_and(V,X) { __atomic_op(X,&,V); }
> -atomic_or(V,X) { __atomic_op(X,|,V); }
> -atomic_xor(V,X) { __atomic_op(X,^,V); }
> -atomic_inc(X) { __atomic_op(X,+,1); }
> -atomic_dec(X) { __atomic_op(X,-,1); }
> -atomic_andnot(V,X) { __atomic_op(X,&~,V); }
> +atomic_add(V,X) { __atomic_op{noreturn}(X,+,V); }
> +atomic_sub(V,X) { __atomic_op{noreturn}(X,-,V); }
> +atomic_and(V,X) { __atomic_op{noreturn}(X,&,V); }
> +atomic_or(V,X) { __atomic_op{noreturn}(X,|,V); }
> +atomic_xor(V,X) { __atomic_op{noreturn}(X,^,V); }
> +atomic_inc(X) { __atomic_op{noreturn}(X,+,1); }
> +atomic_dec(X) { __atomic_op{noreturn}(X,-,1); }
> +atomic_andnot(V,X) { __atomic_op{noreturn}(X,&~,V); }
>
> atomic_add_return(V,X) __atomic_op_return{mb}(X,+,V)
> atomic_add_return_relaxed(V,X) __atomic_op_return{once}(X,+,V)
> @@ -144,3 +144,5 @@ atomic_fetch_andnot(V,X) __atomic_fetch_op{mb}(X,&~,V)
> atomic_fetch_andnot_acquire(V,X) __atomic_fetch_op{acquire}(X,&~,V)
> atomic_fetch_andnot_release(V,X) __atomic_fetch_op{release}(X,&~,V)
> atomic_fetch_andnot_relaxed(V,X) __atomic_fetch_op{once}(X,&~,V)
> +
> +atomic_add_unless(X,V,W) __atomic_add_unless{mb}(X,V,W)
> --
> 2.34.1
>
>
Am 10/29/2024 um 1:04 AM schrieb Boqun Feng: > > One bit below: > > On Mon, Sep 30, 2024 at 12:57:09PM +0200, Jonas Oberhauser wrote: >> ------------------------------------------------------------------------------ >> | RMW ops w/o return value | | >> ------------------------------------------------------------------------------ >> - | atomic_add | R*[noreturn] ->rmw W*[once] | >> + | atomic_add | R*[noreturn] ->rmw W*[noreturn] | > > Not in this patch, but don't you need to update this again to all cap > to match your changes in patch #5? ;-) > Hmmm, probably that is a good idea. I actually had thought about it for some of the other places in the doc that mention the tags, and concluded that we'll just use the semantic tags there. But in fact, this file is about the syntactic representation in herd, and there is no noreturn semantic tag on the W*, so it wouldn't match it even if it were correct. So I think this needs to be addressed in 5/5. jonas
On Wed, Oct 30, 2024 at 12:50:19PM +0100, Jonas Oberhauser wrote: > > > Am 10/29/2024 um 1:04 AM schrieb Boqun Feng: > > > > One bit below: > > > > On Mon, Sep 30, 2024 at 12:57:09PM +0200, Jonas Oberhauser wrote: > > > ------------------------------------------------------------------------------ > > > | RMW ops w/o return value | | > > > ------------------------------------------------------------------------------ > > > - | atomic_add | R*[noreturn] ->rmw W*[once] | > > > + | atomic_add | R*[noreturn] ->rmw W*[noreturn] | > > > > Not in this patch, but don't you need to update this again to all cap > > to match your changes in patch #5? ;-) > > > > Hmmm, probably that is a good idea. > I actually had thought about it for some of the other places in the doc that > mention the tags, and concluded that we'll just use the semantic tags there. > > But in fact, this file is about the syntactic representation in herd, and > there is no noreturn semantic tag on the W*, so it wouldn't match it even if > it were correct. > > So I think this needs to be addressed in 5/5. Thank you for checking! Please send me either a replacement for 5/5 or a patch for me to fold into 5/5. Thanx, Paul
On Mon, Oct 28, 2024 at 05:04:38PM -0700, Boqun Feng wrote:
> On Mon, Sep 30, 2024 at 12:57:09PM +0200, Jonas Oberhauser wrote:
> > A new version of herd7 provides a -lkmmv2 switch which overrides the old herd7
> > behavior of simply ignoring any softcoded tags in the .def and .bell files. We
> > port LKMM to this version of herd7 by providing the switch in linux-kernel.cfg
> > and reporting an error if the LKMM is used without this switch.
> >
> > To preserve the semantics of LKMM, we also softcode the Noreturn tag on atomic
> > RMW which do not return a value and define atomic_add_unless with an Mb tag in
> > linux-kernel.def.
> >
> > We update the herd-representation.txt accordingly and clarify some of the
> > resulting combinations.
> >
> > (To be) Signed-off-by: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>
> > Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
>
> Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
>
> One bit below:
Jonas, if you agree, please feel free to send this as an updated patch
5/5 or as a separate patch. Either way, just let me know!
Thanx, Paul
> > ---
> > .../Documentation/herd-representation.txt | 27 ++++++++++---------
> > tools/memory-model/README | 2 +-
> > tools/memory-model/linux-kernel.bell | 3 +++
> > tools/memory-model/linux-kernel.cfg | 1 +
> > tools/memory-model/linux-kernel.def | 18 +++++++------
> > 5 files changed, 30 insertions(+), 21 deletions(-)
> >
> > diff --git a/tools/memory-model/Documentation/herd-representation.txt b/tools/memory-model/Documentation/herd-representation.txt
> > index ed988906f2b7..7ae1ff3d3769 100644
> > --- a/tools/memory-model/Documentation/herd-representation.txt
> > +++ b/tools/memory-model/Documentation/herd-representation.txt
> > @@ -18,6 +18,11 @@
> > #
> > # By convention, a blank line in a cell means "same as the preceding line".
> > #
> > +# Note that the syntactic representation does not always match the sets and
> > +# relations in linux-kernel.cat, due to redefinitions in linux-kernel.bell and
> > +# lock.cat. For example, the po link between LKR and LKW is upgraded to an rmw
> > +# link, and W[acquire] are not included in the Acquire set.
> > +#
> > # Disclaimer. The table includes representations of "add" and "and" operations;
> > # corresponding/identical representations of "sub", "inc", "dec" and "or", "xor",
> > # "andnot" operations are omitted.
> > @@ -60,14 +65,13 @@
> > ------------------------------------------------------------------------------
> > | RMW ops w/o return value | |
> > ------------------------------------------------------------------------------
> > - | atomic_add | R*[noreturn] ->rmw W*[once] |
> > + | atomic_add | R*[noreturn] ->rmw W*[noreturn] |
>
> Not in this patch, but don't you need to update this again to all cap
> to match your changes in patch #5? ;-)
>
> Regards,
> Boqun
>
> > | atomic_and | |
> > | spin_lock | LKR ->po LKW |
> > ------------------------------------------------------------------------------
> > | RMW ops w/ return value | |
> > ------------------------------------------------------------------------------
> > - | atomic_add_return | F[mb] ->po R*[once] |
> > - | | ->rmw W*[once] ->po F[mb] |
> > + | atomic_add_return | R*[mb] ->rmw W*[mb] |
> > | atomic_fetch_add | |
> > | atomic_fetch_and | |
> > | atomic_xchg | |
> > @@ -79,13 +83,13 @@
> > | atomic_xchg_relaxed | |
> > | xchg_relaxed | |
> > | atomic_add_negative_relaxed | |
> > - | atomic_add_return_acquire | R*[acquire] ->rmw W*[once] |
> > + | atomic_add_return_acquire | R*[acquire] ->rmw W*[acquire] |
> > | atomic_fetch_add_acquire | |
> > | atomic_fetch_and_acquire | |
> > | atomic_xchg_acquire | |
> > | xchg_acquire | |
> > | atomic_add_negative_acquire | |
> > - | atomic_add_return_release | R*[once] ->rmw W*[release] |
> > + | atomic_add_return_release | R*[release] ->rmw W*[release] |
> > | atomic_fetch_add_release | |
> > | atomic_fetch_and_release | |
> > | atomic_xchg_release | |
> > @@ -94,17 +98,16 @@
> > ------------------------------------------------------------------------------
> > | Conditional RMW ops | |
> > ------------------------------------------------------------------------------
> > - | atomic_cmpxchg | On success: F[mb] ->po R*[once] |
> > - | | ->rmw W*[once] ->po F[mb] |
> > - | | On failure: R*[once] |
> > + | atomic_cmpxchg | On success: R*[mb] ->rmw W*[mb] |
> > + | | On failure: R*[mb] |
> > | cmpxchg | |
> > | atomic_add_unless | |
> > | atomic_cmpxchg_relaxed | On success: R*[once] ->rmw W*[once] |
> > | | On failure: R*[once] |
> > - | atomic_cmpxchg_acquire | On success: R*[acquire] ->rmw W*[once] |
> > - | | On failure: R*[once] |
> > - | atomic_cmpxchg_release | On success: R*[once] ->rmw W*[release] |
> > - | | On failure: R*[once] |
> > + | atomic_cmpxchg_acquire | On success: R*[acquire] ->rmw W*[acquire] |
> > + | | On failure: R*[acquire] |
> > + | atomic_cmpxchg_release | On success: R*[release] ->rmw W*[release] |
> > + | | On failure: R*[release] |
> > | spin_trylock | On success: LKR ->po LKW |
> > | | On failure: LF |
> > ------------------------------------------------------------------------------
> > diff --git a/tools/memory-model/README b/tools/memory-model/README
> > index dab38904206a..59bc15edeb8a 100644
> > --- a/tools/memory-model/README
> > +++ b/tools/memory-model/README
> > @@ -20,7 +20,7 @@ that litmus test to be exercised within the Linux kernel.
> > REQUIREMENTS
> > ============
> >
> > -Version 7.52 or higher of the "herd7" and "klitmus7" tools must be
> > +Version 7.58 or higher of the "herd7" and "klitmus7" tools must be
> > downloaded separately:
> >
> > https://github.com/herd/herdtools7
> > diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
> > index 7c9ae48b9437..8ae47545df97 100644
> > --- a/tools/memory-model/linux-kernel.bell
> > +++ b/tools/memory-model/linux-kernel.bell
> > @@ -94,3 +94,6 @@ let carry-dep = (data ; [~ Srcu-unlock] ; rfi)*
> > let addr = carry-dep ; addr
> > let ctrl = carry-dep ; ctrl
> > let data = carry-dep ; data
> > +
> > +flag ~empty (if "lkmmv2" then 0 else _)
> > + as this-model-requires-variant-higher-than-lkmmv1
> > diff --git a/tools/memory-model/linux-kernel.cfg b/tools/memory-model/linux-kernel.cfg
> > index 3c8098e99f41..69b04f3aad73 100644
> > --- a/tools/memory-model/linux-kernel.cfg
> > +++ b/tools/memory-model/linux-kernel.cfg
> > @@ -1,6 +1,7 @@
> > macros linux-kernel.def
> > bell linux-kernel.bell
> > model linux-kernel.cat
> > +variant lkmmv2
> > graph columns
> > squished true
> > showevents noregs
> > diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
> > index a12b96c547b7..d7279a357cba 100644
> > --- a/tools/memory-model/linux-kernel.def
> > +++ b/tools/memory-model/linux-kernel.def
> > @@ -63,14 +63,14 @@ atomic_set(X,V) { WRITE_ONCE(*X,V); }
> > atomic_read_acquire(X) smp_load_acquire(X)
> > atomic_set_release(X,V) { smp_store_release(X,V); }
> >
> > -atomic_add(V,X) { __atomic_op(X,+,V); }
> > -atomic_sub(V,X) { __atomic_op(X,-,V); }
> > -atomic_and(V,X) { __atomic_op(X,&,V); }
> > -atomic_or(V,X) { __atomic_op(X,|,V); }
> > -atomic_xor(V,X) { __atomic_op(X,^,V); }
> > -atomic_inc(X) { __atomic_op(X,+,1); }
> > -atomic_dec(X) { __atomic_op(X,-,1); }
> > -atomic_andnot(V,X) { __atomic_op(X,&~,V); }
> > +atomic_add(V,X) { __atomic_op{noreturn}(X,+,V); }
> > +atomic_sub(V,X) { __atomic_op{noreturn}(X,-,V); }
> > +atomic_and(V,X) { __atomic_op{noreturn}(X,&,V); }
> > +atomic_or(V,X) { __atomic_op{noreturn}(X,|,V); }
> > +atomic_xor(V,X) { __atomic_op{noreturn}(X,^,V); }
> > +atomic_inc(X) { __atomic_op{noreturn}(X,+,1); }
> > +atomic_dec(X) { __atomic_op{noreturn}(X,-,1); }
> > +atomic_andnot(V,X) { __atomic_op{noreturn}(X,&~,V); }
> >
> > atomic_add_return(V,X) __atomic_op_return{mb}(X,+,V)
> > atomic_add_return_relaxed(V,X) __atomic_op_return{once}(X,+,V)
> > @@ -144,3 +144,5 @@ atomic_fetch_andnot(V,X) __atomic_fetch_op{mb}(X,&~,V)
> > atomic_fetch_andnot_acquire(V,X) __atomic_fetch_op{acquire}(X,&~,V)
> > atomic_fetch_andnot_release(V,X) __atomic_fetch_op{release}(X,&~,V)
> > atomic_fetch_andnot_relaxed(V,X) __atomic_fetch_op{once}(X,&~,V)
> > +
> > +atomic_add_unless(X,V,W) __atomic_add_unless{mb}(X,V,W)
> > --
> > 2.34.1
> >
> >
On 9/30/2024 12:57 PM, Jonas Oberhauser wrote:
> A new version of herd7 provides a -lkmmv2 switch which overrides the old herd7
> behavior of simply ignoring any softcoded tags in the .def and .bell files. We
> port LKMM to this version of herd7 by providing the switch in linux-kernel.cfg
> and reporting an error if the LKMM is used without this switch.
The changes required for this patch were already merged to herd7.
>
> To preserve the semantics of LKMM, we also softcode the Noreturn tag on atomic
> RMW which do not return a value and define atomic_add_unless with an Mb tag in
> linux-kernel.def.
>
> We update the herd-representation.txt accordingly and clarify some of the
> resulting combinations.
>
> (To be) Signed-off-by: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>
Signed-off-by: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>
> Signed-off-by: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
> ---
> .../Documentation/herd-representation.txt | 27 ++++++++++---------
> tools/memory-model/README | 2 +-
> tools/memory-model/linux-kernel.bell | 3 +++
> tools/memory-model/linux-kernel.cfg | 1 +
> tools/memory-model/linux-kernel.def | 18 +++++++------
> 5 files changed, 30 insertions(+), 21 deletions(-)
>
> diff --git a/tools/memory-model/Documentation/herd-representation.txt b/tools/memory-model/Documentation/herd-representation.txt
> index ed988906f2b7..7ae1ff3d3769 100644
> --- a/tools/memory-model/Documentation/herd-representation.txt
> +++ b/tools/memory-model/Documentation/herd-representation.txt
> @@ -18,6 +18,11 @@
> #
> # By convention, a blank line in a cell means "same as the preceding line".
> #
> +# Note that the syntactic representation does not always match the sets and
> +# relations in linux-kernel.cat, due to redefinitions in linux-kernel.bell and
> +# lock.cat. For example, the po link between LKR and LKW is upgraded to an rmw
> +# link, and W[acquire] are not included in the Acquire set.
> +#
> # Disclaimer. The table includes representations of "add" and "and" operations;
> # corresponding/identical representations of "sub", "inc", "dec" and "or", "xor",
> # "andnot" operations are omitted.
> @@ -60,14 +65,13 @@
> ------------------------------------------------------------------------------
> | RMW ops w/o return value | |
> ------------------------------------------------------------------------------
> - | atomic_add | R*[noreturn] ->rmw W*[once] |
> + | atomic_add | R*[noreturn] ->rmw W*[noreturn] |
> | atomic_and | |
> | spin_lock | LKR ->po LKW |
> ------------------------------------------------------------------------------
> | RMW ops w/ return value | |
> ------------------------------------------------------------------------------
> - | atomic_add_return | F[mb] ->po R*[once] |
> - | | ->rmw W*[once] ->po F[mb] |
> + | atomic_add_return | R*[mb] ->rmw W*[mb] |
> | atomic_fetch_add | |
> | atomic_fetch_and | |
> | atomic_xchg | |
> @@ -79,13 +83,13 @@
> | atomic_xchg_relaxed | |
> | xchg_relaxed | |
> | atomic_add_negative_relaxed | |
> - | atomic_add_return_acquire | R*[acquire] ->rmw W*[once] |
> + | atomic_add_return_acquire | R*[acquire] ->rmw W*[acquire] |
> | atomic_fetch_add_acquire | |
> | atomic_fetch_and_acquire | |
> | atomic_xchg_acquire | |
> | xchg_acquire | |
> | atomic_add_negative_acquire | |
> - | atomic_add_return_release | R*[once] ->rmw W*[release] |
> + | atomic_add_return_release | R*[release] ->rmw W*[release] |
> | atomic_fetch_add_release | |
> | atomic_fetch_and_release | |
> | atomic_xchg_release | |
> @@ -94,17 +98,16 @@
> ------------------------------------------------------------------------------
> | Conditional RMW ops | |
> ------------------------------------------------------------------------------
> - | atomic_cmpxchg | On success: F[mb] ->po R*[once] |
> - | | ->rmw W*[once] ->po F[mb] |
> - | | On failure: R*[once] |
> + | atomic_cmpxchg | On success: R*[mb] ->rmw W*[mb] |
> + | | On failure: R*[mb] |
> | cmpxchg | |
> | atomic_add_unless | |
> | atomic_cmpxchg_relaxed | On success: R*[once] ->rmw W*[once] |
> | | On failure: R*[once] |
> - | atomic_cmpxchg_acquire | On success: R*[acquire] ->rmw W*[once] |
> - | | On failure: R*[once] |
> - | atomic_cmpxchg_release | On success: R*[once] ->rmw W*[release] |
> - | | On failure: R*[once] |
> + | atomic_cmpxchg_acquire | On success: R*[acquire] ->rmw W*[acquire] |
> + | | On failure: R*[acquire] |
> + | atomic_cmpxchg_release | On success: R*[release] ->rmw W*[release] |
> + | | On failure: R*[release] |
> | spin_trylock | On success: LKR ->po LKW |
> | | On failure: LF |
> ------------------------------------------------------------------------------
> diff --git a/tools/memory-model/README b/tools/memory-model/README
> index dab38904206a..59bc15edeb8a 100644
> --- a/tools/memory-model/README
> +++ b/tools/memory-model/README
> @@ -20,7 +20,7 @@ that litmus test to be exercised within the Linux kernel.
> REQUIREMENTS
> ============
>
> -Version 7.52 or higher of the "herd7" and "klitmus7" tools must be
> +Version 7.58 or higher of the "herd7" and "klitmus7" tools must be
> downloaded separately:
>
> https://github.com/herd/herdtools7
> diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
> index 7c9ae48b9437..8ae47545df97 100644
> --- a/tools/memory-model/linux-kernel.bell
> +++ b/tools/memory-model/linux-kernel.bell
> @@ -94,3 +94,6 @@ let carry-dep = (data ; [~ Srcu-unlock] ; rfi)*
> let addr = carry-dep ; addr
> let ctrl = carry-dep ; ctrl
> let data = carry-dep ; data
> +
> +flag ~empty (if "lkmmv2" then 0 else _)
> + as this-model-requires-variant-higher-than-lkmmv1
> diff --git a/tools/memory-model/linux-kernel.cfg b/tools/memory-model/linux-kernel.cfg
> index 3c8098e99f41..69b04f3aad73 100644
> --- a/tools/memory-model/linux-kernel.cfg
> +++ b/tools/memory-model/linux-kernel.cfg
> @@ -1,6 +1,7 @@
> macros linux-kernel.def
> bell linux-kernel.bell
> model linux-kernel.cat
> +variant lkmmv2
> graph columns
> squished true
> showevents noregs
> diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
> index a12b96c547b7..d7279a357cba 100644
> --- a/tools/memory-model/linux-kernel.def
> +++ b/tools/memory-model/linux-kernel.def
> @@ -63,14 +63,14 @@ atomic_set(X,V) { WRITE_ONCE(*X,V); }
> atomic_read_acquire(X) smp_load_acquire(X)
> atomic_set_release(X,V) { smp_store_release(X,V); }
>
> -atomic_add(V,X) { __atomic_op(X,+,V); }
> -atomic_sub(V,X) { __atomic_op(X,-,V); }
> -atomic_and(V,X) { __atomic_op(X,&,V); }
> -atomic_or(V,X) { __atomic_op(X,|,V); }
> -atomic_xor(V,X) { __atomic_op(X,^,V); }
> -atomic_inc(X) { __atomic_op(X,+,1); }
> -atomic_dec(X) { __atomic_op(X,-,1); }
> -atomic_andnot(V,X) { __atomic_op(X,&~,V); }
> +atomic_add(V,X) { __atomic_op{noreturn}(X,+,V); }
> +atomic_sub(V,X) { __atomic_op{noreturn}(X,-,V); }
> +atomic_and(V,X) { __atomic_op{noreturn}(X,&,V); }
> +atomic_or(V,X) { __atomic_op{noreturn}(X,|,V); }
> +atomic_xor(V,X) { __atomic_op{noreturn}(X,^,V); }
> +atomic_inc(X) { __atomic_op{noreturn}(X,+,1); }
> +atomic_dec(X) { __atomic_op{noreturn}(X,-,1); }
> +atomic_andnot(V,X) { __atomic_op{noreturn}(X,&~,V); }
>
> atomic_add_return(V,X) __atomic_op_return{mb}(X,+,V)
> atomic_add_return_relaxed(V,X) __atomic_op_return{once}(X,+,V)
> @@ -144,3 +144,5 @@ atomic_fetch_andnot(V,X) __atomic_fetch_op{mb}(X,&~,V)
> atomic_fetch_andnot_acquire(V,X) __atomic_fetch_op{acquire}(X,&~,V)
> atomic_fetch_andnot_release(V,X) __atomic_fetch_op{release}(X,&~,V)
> atomic_fetch_andnot_relaxed(V,X) __atomic_fetch_op{once}(X,&~,V)
> +
> +atomic_add_unless(X,V,W) __atomic_add_unless{mb}(X,V,W)
© 2016 - 2024 Red Hat, Inc.