tools/memory-model/Documentation/README | 7 +- .../Documentation/herd-representation.txt | 106 ++++++++++++++++++ 2 files changed, 112 insertions(+), 1 deletion(-) create mode 100644 tools/memory-model/Documentation/herd-representation.txt
tools/memory-model/ and herdtool7 are closely linked: the latter is
responsible for (pre)processing each C-like macro of a litmus test,
and for providing the LKMM with a set of events, or "representation",
corresponding to the given macro. Provide herd-representation.txt
to document the representations of the concurrency macros, following
their "classification" in Documentation/atomic_t.txt.
Suggested-by: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>
Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
---
Changes since v2 [1]:
- drop lk-rmw links
Changes since v1 [2]:
- add legenda/notations
- add some SRCU, locking macros
- update formatting of failure cases
- update README file
[1] https://lore.kernel.org/lkml/20240605134918.365579-1-parri.andrea@gmail.com/
[2] https://lore.kernel.org/lkml/20240524151356.236071-1-parri.andrea@gmail.com/
tools/memory-model/Documentation/README | 7 +-
.../Documentation/herd-representation.txt | 106 ++++++++++++++++++
2 files changed, 112 insertions(+), 1 deletion(-)
create mode 100644 tools/memory-model/Documentation/herd-representation.txt
diff --git a/tools/memory-model/Documentation/README b/tools/memory-model/Documentation/README
index 304162743a5b8..44e7dae73b296 100644
--- a/tools/memory-model/Documentation/README
+++ b/tools/memory-model/Documentation/README
@@ -33,7 +33,8 @@ o You are familiar with Linux-kernel concurrency and the use of
o You are familiar with Linux-kernel concurrency and the use
of LKMM, and would like to learn about LKMM's requirements,
- rationale, and implementation: explanation.txt
+ rationale, and implementation: explanation.txt and
+ herd-representation.txt
o You are interested in the publications related to LKMM, including
hardware manuals, academic literature, standards-committee
@@ -61,6 +62,10 @@ control-dependencies.txt
explanation.txt
Detailed description of the memory model.
+herd-representation.txt
+ The (abstract) representation of the Linux-kernel concurrency
+ primitives in terms of events.
+
litmus-tests.txt
The format, features, capabilities, and limitations of the litmus
tests that LKMM can evaluate.
diff --git a/tools/memory-model/Documentation/herd-representation.txt b/tools/memory-model/Documentation/herd-representation.txt
new file mode 100644
index 0000000000000..2fe270e902635
--- /dev/null
+++ b/tools/memory-model/Documentation/herd-representation.txt
@@ -0,0 +1,106 @@
+#
+# Legenda:
+# R, a Load event
+# W, a Store event
+# F, a Fence event
+# LKR, a Lock-Read event
+# LKW, a Lock-Write event
+# UL, an Unlock event
+# LF, a Lock-Fail event
+# RL, a Read-Locked event
+# RU, a Read-Unlocked event
+# R*, a Load event included in RMW
+# W*, a Store event included in RMW
+# SRCU, a Sleepable-Read-Copy-Update event
+#
+# po, a Program-Order link
+# rmw, a Read-Modify-Write link
+#
+# By convention, a blank entry/representation means "same as the preceding entry".
+#
+ ------------------------------------------------------------------------------
+ | C macro | Events |
+ ------------------------------------------------------------------------------
+ | Non-RMW ops | |
+ ------------------------------------------------------------------------------
+ | READ_ONCE | R[once] |
+ | atomic_read | |
+ | WRITE_ONCE | W[once] |
+ | atomic_set | |
+ | smp_load_acquire | R[acquire] |
+ | atomic_read_acquire | |
+ | smp_store_release | W[release] |
+ | atomic_set_release | |
+ | smp_store_mb | W[once] ->po F[mb] |
+ | smp_mb | F[mb] |
+ | smp_rmb | F[rmb] |
+ | smp_wmb | F[wmb] |
+ | smp_mb__before_atomic | F[before-atomic] |
+ | smp_mb__after_atomic | F[after-atomic] |
+ | spin_unlock | UL |
+ | spin_is_locked | On success: RL |
+ | | On failure: RU |
+ | smp_mb__after_spinlock | F[after-spinlock] |
+ | smp_mb__after_unlock_lock | F[after-unlock-lock] |
+ | rcu_read_lock | F[rcu-lock] |
+ | rcu_read_unlock | F[rcu-unlock] |
+ | synchronize_rcu | F[sync-rcu] |
+ | rcu_dereference | R[once] |
+ | rcu_assign_pointer | W[release] |
+ | srcu_read_lock | R[srcu-lock] |
+ | srcu_down_read | |
+ | srcu_read_unlock | W[srcu-unlock] |
+ | srcu_up_read | |
+ | synchronize_srcu | SRCU[sync-srcu] |
+ | smp_mb__after_srcu_read_unlock | F[after-srcu-read-unlock] |
+ ------------------------------------------------------------------------------
+ | RMW ops w/o return value | |
+ ------------------------------------------------------------------------------
+ | atomic_add | R*[noreturn] ->rmw W*[once] |
+ | 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_fetch_add | |
+ | atomic_fetch_and | |
+ | atomic_xchg | |
+ | xchg | |
+ | atomic_add_negative | |
+ | atomic_add_return_relaxed | R*[once] ->rmw W*[once] |
+ | atomic_fetch_add_relaxed | |
+ | atomic_fetch_and_relaxed | |
+ | atomic_xchg_relaxed | |
+ | xchg_relaxed | |
+ | atomic_add_negative_relaxed | |
+ | atomic_add_return_acquire | R*[acquire] ->rmw W*[once] |
+ | 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_fetch_add_release | |
+ | atomic_fetch_and_release | |
+ | atomic_xchg_release | |
+ | xchg_release | |
+ | atomic_add_negative_release | |
+ ------------------------------------------------------------------------------
+ | Conditional RMW ops | |
+ ------------------------------------------------------------------------------
+ | atomic_cmpxchg | On success: F[mb] ->po R*[once] |
+ | | ->rmw W*[once] ->po F[mb] |
+ | | On failure: R*[once] |
+ | 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] |
+ | spin_trylock | On success: LKR ->po LKW |
+ | | On failure: LF |
+ ------------------------------------------------------------------------------
--
2.34.1On Mon, Jun 17, 2024 at 10:17:59PM +0200, Andrea Parri wrote:
> tools/memory-model/ and herdtool7 are closely linked: the latter is
> responsible for (pre)processing each C-like macro of a litmus test,
> and for providing the LKMM with a set of events, or "representation",
> corresponding to the given macro. Provide herd-representation.txt
> to document the representations of the concurrency macros, following
> their "classification" in Documentation/atomic_t.txt.
>
> Suggested-by: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>
> Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
Queued, thank you!
I added Boqun's and Hernan's Reviewed-by tags and did the usual
wordsmithing. Please check below to make sure that I did not mess
anything up.
Also, Puranjay added atomic_and()/or()/xor() and add_negative, which
is slated to go in to the next merge window:
be98107ab8a5 ("tools/memory-model: Add atomic_and()/or()/xor() and add_negative")
Would you like to add the corresponding lines to this table?
Thanx, Paul
------------------------------------------------------------------------
commit 0e72657b7cb518ef8d996e2bf9bf14676da9af3f
Author: Andrea Parri <parri.andrea@gmail.com>
Date: Mon Jun 17 22:17:59 2024 +0200
tools/memory-model: Document herd7 (abstract) representation
The Linux-kernel memory model (LKMM) source code and the herd7 tool are
closely linked in that the latter is responsible for (pre)processing
each C-like macro of a litmus test, and for providing the LKMM with a
set of events, or "representation", corresponding to the given macro.
This commit therefore provides herd-representation.txt to document
the representations of the concurrency macros, following their
"classification" in Documentation/atomic_t.txt.
Suggested-by: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>
Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Reviewed-by: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
diff --git a/tools/memory-model/Documentation/README b/tools/memory-model/Documentation/README
index 304162743a5b8..44e7dae73b296 100644
--- a/tools/memory-model/Documentation/README
+++ b/tools/memory-model/Documentation/README
@@ -33,7 +33,8 @@ o You are familiar with Linux-kernel concurrency and the use of
o You are familiar with Linux-kernel concurrency and the use
of LKMM, and would like to learn about LKMM's requirements,
- rationale, and implementation: explanation.txt
+ rationale, and implementation: explanation.txt and
+ herd-representation.txt
o You are interested in the publications related to LKMM, including
hardware manuals, academic literature, standards-committee
@@ -61,6 +62,10 @@ control-dependencies.txt
explanation.txt
Detailed description of the memory model.
+herd-representation.txt
+ The (abstract) representation of the Linux-kernel concurrency
+ primitives in terms of events.
+
litmus-tests.txt
The format, features, capabilities, and limitations of the litmus
tests that LKMM can evaluate.
diff --git a/tools/memory-model/Documentation/herd-representation.txt b/tools/memory-model/Documentation/herd-representation.txt
new file mode 100644
index 0000000000000..6f09df2372d2f
--- /dev/null
+++ b/tools/memory-model/Documentation/herd-representation.txt
@@ -0,0 +1,106 @@
+#
+# Legend:
+# R, a Load event
+# W, a Store event
+# F, a Fence event
+# LKR, a Lock-Read event
+# LKW, a Lock-Write event
+# UL, an Unlock event
+# LF, a Lock-Fail event
+# RL, a Read-Locked event
+# RU, a Read-Unlocked event
+# R*, a Load event included in RMW
+# W*, a Store event included in RMW
+# SRCU, a Sleepable-Read-Copy-Update event
+#
+# po, a Program-Order link
+# rmw, a Read-Modify-Write link
+#
+# By convention, a blank line in a cell means "same as the preceding line".
+#
+ ------------------------------------------------------------------------------
+ | C macro | Events |
+ ------------------------------------------------------------------------------
+ | Non-RMW ops | |
+ ------------------------------------------------------------------------------
+ | READ_ONCE | R[once] |
+ | atomic_read | |
+ | WRITE_ONCE | W[once] |
+ | atomic_set | |
+ | smp_load_acquire | R[acquire] |
+ | atomic_read_acquire | |
+ | smp_store_release | W[release] |
+ | atomic_set_release | |
+ | smp_store_mb | W[once] ->po F[mb] |
+ | smp_mb | F[mb] |
+ | smp_rmb | F[rmb] |
+ | smp_wmb | F[wmb] |
+ | smp_mb__before_atomic | F[before-atomic] |
+ | smp_mb__after_atomic | F[after-atomic] |
+ | spin_unlock | UL |
+ | spin_is_locked | On success: RL |
+ | | On failure: RU |
+ | smp_mb__after_spinlock | F[after-spinlock] |
+ | smp_mb__after_unlock_lock | F[after-unlock-lock] |
+ | rcu_read_lock | F[rcu-lock] |
+ | rcu_read_unlock | F[rcu-unlock] |
+ | synchronize_rcu | F[sync-rcu] |
+ | rcu_dereference | R[once] |
+ | rcu_assign_pointer | W[release] |
+ | srcu_read_lock | R[srcu-lock] |
+ | srcu_down_read | |
+ | srcu_read_unlock | W[srcu-unlock] |
+ | srcu_up_read | |
+ | synchronize_srcu | SRCU[sync-srcu] |
+ | smp_mb__after_srcu_read_unlock | F[after-srcu-read-unlock] |
+ ------------------------------------------------------------------------------
+ | RMW ops w/o return value | |
+ ------------------------------------------------------------------------------
+ | atomic_add | R*[noreturn] ->rmw W*[once] |
+ | 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_fetch_add | |
+ | atomic_fetch_and | |
+ | atomic_xchg | |
+ | xchg | |
+ | atomic_add_negative | |
+ | atomic_add_return_relaxed | R*[once] ->rmw W*[once] |
+ | atomic_fetch_add_relaxed | |
+ | atomic_fetch_and_relaxed | |
+ | atomic_xchg_relaxed | |
+ | xchg_relaxed | |
+ | atomic_add_negative_relaxed | |
+ | atomic_add_return_acquire | R*[acquire] ->rmw W*[once] |
+ | 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_fetch_add_release | |
+ | atomic_fetch_and_release | |
+ | atomic_xchg_release | |
+ | xchg_release | |
+ | atomic_add_negative_release | |
+ ------------------------------------------------------------------------------
+ | Conditional RMW ops | |
+ ------------------------------------------------------------------------------
+ | atomic_cmpxchg | On success: F[mb] ->po R*[once] |
+ | | ->rmw W*[once] ->po F[mb] |
+ | | On failure: R*[once] |
+ | 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] |
+ | spin_trylock | On success: LKR ->po LKW |
+ | | On failure: LF |
+ ------------------------------------------------------------------------------
> Queued, thank you!
>
> I added Boqun's and Hernan's Reviewed-by tags and did the usual
> wordsmithing. Please check below to make sure that I did not mess
> anything up.
Thanks! That does look good to me.
It is missing the small addition to the rmw description discussed
earlier in the thread [1]: feel free to squash it in your commit if
that works for you (alternatively, I can respin the entire thing
with that, JLMK what you prefer).
> Also, Puranjay added atomic_and()/or()/xor() and add_negative, which
> is slated to go in to the next merge window:
>
> be98107ab8a5 ("tools/memory-model: Add atomic_and()/or()/xor() and add_negative")
>
> Would you like to add the corresponding lines to this table?
atomic_and() and atomic_add_negative() (together with its variants)
should be listed in the table.
I did promise myself that I would have not done "or", "xor", "andnot"
as well as "sub", "inc", "dec", but never say never! :-) Alternatively,
we could perhaps add a note along the lines of
The table includes "add" and "and" operations; analogous/identical
representations for "sub", "inc", "dec", "or", "xor" and "andnot"
operations are omitted.
Andrea
[1] https://lore.kernel.org/ZnFZPJlILp5B9scN@andrea
On Tue, Jun 18, 2024 at 08:41:15PM +0200, Andrea Parri wrote:
> > Queued, thank you!
> >
> > I added Boqun's and Hernan's Reviewed-by tags and did the usual
> > wordsmithing. Please check below to make sure that I did not mess
> > anything up.
>
> Thanks! That does look good to me.
>
> It is missing the small addition to the rmw description discussed
> earlier in the thread [1]: feel free to squash it in your commit if
> that works for you (alternatively, I can respin the entire thing
> with that, JLMK what you prefer).
Please respin and I will replace the one that I have.
I clearly should have read the chain more carefully. ;-)
> > Also, Puranjay added atomic_and()/or()/xor() and add_negative, which
> > is slated to go in to the next merge window:
> >
> > be98107ab8a5 ("tools/memory-model: Add atomic_and()/or()/xor() and add_negative")
> >
> > Would you like to add the corresponding lines to this table?
>
> atomic_and() and atomic_add_negative() (together with its variants)
> should be listed in the table.
>
> I did promise myself that I would have not done "or", "xor", "andnot"
> as well as "sub", "inc", "dec", but never say never! :-) Alternatively,
> we could perhaps add a note along the lines of
>
> The table includes "add" and "and" operations; analogous/identical
> representations for "sub", "inc", "dec", "or", "xor" and "andnot"
> operations are omitted.
I am OK either way. The second approach could be used to shrink
the "RMW ops w/ return value" section, if desired.
Thanx, Paul
> Andrea
>
> [1] https://lore.kernel.org/ZnFZPJlILp5B9scN@andrea
On Mon, Jun 17, 2024 at 10:17:59PM +0200, Andrea Parri wrote: > tools/memory-model/ and herdtool7 are closely linked: the latter is > responsible for (pre)processing each C-like macro of a litmus test, > and for providing the LKMM with a set of events, or "representation", > corresponding to the given macro. Provide herd-representation.txt > to document the representations of the concurrency macros, following > their "classification" in Documentation/atomic_t.txt. > > Suggested-by: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com> > Signed-off-by: Andrea Parri <parri.andrea@gmail.com> Reviewed-by: Boqun Feng <boqun.feng@gmail.com> I have a question below... > --- > Changes since v2 [1]: > - drop lk-rmw links > > Changes since v1 [2]: > - add legenda/notations > - add some SRCU, locking macros > - update formatting of failure cases > - update README file > > [1] https://lore.kernel.org/lkml/20240605134918.365579-1-parri.andrea@gmail.com/ > [2] https://lore.kernel.org/lkml/20240524151356.236071-1-parri.andrea@gmail.com/ > > tools/memory-model/Documentation/README | 7 +- > .../Documentation/herd-representation.txt | 106 ++++++++++++++++++ > 2 files changed, 112 insertions(+), 1 deletion(-) > create mode 100644 tools/memory-model/Documentation/herd-representation.txt > > diff --git a/tools/memory-model/Documentation/README b/tools/memory-model/Documentation/README > index 304162743a5b8..44e7dae73b296 100644 > --- a/tools/memory-model/Documentation/README > +++ b/tools/memory-model/Documentation/README > @@ -33,7 +33,8 @@ o You are familiar with Linux-kernel concurrency and the use of > > o You are familiar with Linux-kernel concurrency and the use > of LKMM, and would like to learn about LKMM's requirements, > - rationale, and implementation: explanation.txt > + rationale, and implementation: explanation.txt and > + herd-representation.txt > > o You are interested in the publications related to LKMM, including > hardware manuals, academic literature, standards-committee > @@ -61,6 +62,10 @@ control-dependencies.txt > explanation.txt > Detailed description of the memory model. > > +herd-representation.txt > + The (abstract) representation of the Linux-kernel concurrency > + primitives in terms of events. > + > litmus-tests.txt > The format, features, capabilities, and limitations of the litmus > tests that LKMM can evaluate. > diff --git a/tools/memory-model/Documentation/herd-representation.txt b/tools/memory-model/Documentation/herd-representation.txt > new file mode 100644 > index 0000000000000..2fe270e902635 > --- /dev/null > +++ b/tools/memory-model/Documentation/herd-representation.txt > @@ -0,0 +1,106 @@ > +# > +# Legenda: > +# R, a Load event > +# W, a Store event > +# F, a Fence event > +# LKR, a Lock-Read event > +# LKW, a Lock-Write event > +# UL, an Unlock event > +# LF, a Lock-Fail event > +# RL, a Read-Locked event > +# RU, a Read-Unlocked event > +# R*, a Load event included in RMW > +# W*, a Store event included in RMW > +# SRCU, a Sleepable-Read-Copy-Update event > +# > +# po, a Program-Order link > +# rmw, a Read-Modify-Write link > +# > +# By convention, a blank entry/representation means "same as the preceding entry". > +# > + ------------------------------------------------------------------------------ > + | C macro | Events | > + ------------------------------------------------------------------------------ > + | Non-RMW ops | | > + ------------------------------------------------------------------------------ > + | READ_ONCE | R[once] | > + | atomic_read | | > + | WRITE_ONCE | W[once] | > + | atomic_set | | > + | smp_load_acquire | R[acquire] | > + | atomic_read_acquire | | > + | smp_store_release | W[release] | > + | atomic_set_release | | > + | smp_store_mb | W[once] ->po F[mb] | > + | smp_mb | F[mb] | > + | smp_rmb | F[rmb] | > + | smp_wmb | F[wmb] | > + | smp_mb__before_atomic | F[before-atomic] | > + | smp_mb__after_atomic | F[after-atomic] | > + | spin_unlock | UL | > + | spin_is_locked | On success: RL | > + | | On failure: RU | > + | smp_mb__after_spinlock | F[after-spinlock] | > + | smp_mb__after_unlock_lock | F[after-unlock-lock] | > + | rcu_read_lock | F[rcu-lock] | > + | rcu_read_unlock | F[rcu-unlock] | > + | synchronize_rcu | F[sync-rcu] | > + | rcu_dereference | R[once] | > + | rcu_assign_pointer | W[release] | > + | srcu_read_lock | R[srcu-lock] | > + | srcu_down_read | | > + | srcu_read_unlock | W[srcu-unlock] | > + | srcu_up_read | | > + | synchronize_srcu | SRCU[sync-srcu] | > + | smp_mb__after_srcu_read_unlock | F[after-srcu-read-unlock] | > + ------------------------------------------------------------------------------ > + | RMW ops w/o return value | | > + ------------------------------------------------------------------------------ > + | atomic_add | R*[noreturn] ->rmw W*[once] | > + | 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] | Just to double check, there is also a ->po relation between R*[once] and W*[once], right? It might not be important right now, but it's important when we move to what Jonas is proposing: https://lore.kernel.org/lkml/20240604152922.495908-1-jonas.oberhauser@huaweicloud.com/ So just check with you ;-) Thanks! Regards, Boqun > + | atomic_fetch_add | | > + | atomic_fetch_and | | > + | atomic_xchg | | > + | xchg | | > + | atomic_add_negative | | > + | atomic_add_return_relaxed | R*[once] ->rmw W*[once] | > + | atomic_fetch_add_relaxed | | > + | atomic_fetch_and_relaxed | | > + | atomic_xchg_relaxed | | > + | xchg_relaxed | | > + | atomic_add_negative_relaxed | | > + | atomic_add_return_acquire | R*[acquire] ->rmw W*[once] | > + | 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_fetch_add_release | | > + | atomic_fetch_and_release | | > + | atomic_xchg_release | | > + | xchg_release | | > + | atomic_add_negative_release | | > + ------------------------------------------------------------------------------ > + | Conditional RMW ops | | > + ------------------------------------------------------------------------------ > + | atomic_cmpxchg | On success: F[mb] ->po R*[once] | > + | | ->rmw W*[once] ->po F[mb] | > + | | On failure: R*[once] | > + | 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] | > + | spin_trylock | On success: LKR ->po LKW | > + | | On failure: LF | > + ------------------------------------------------------------------------------ > -- > 2.34.1 >
On 6/18/2024 12:53 AM, Boqun Feng wrote: > On Mon, Jun 17, 2024 at 10:17:59PM +0200, Andrea Parri wrote: >> tools/memory-model/ and herdtool7 are closely linked: the latter is >> responsible for (pre)processing each C-like macro of a litmus test, >> and for providing the LKMM with a set of events, or "representation", >> corresponding to the given macro. Provide herd-representation.txt >> to document the representations of the concurrency macros, following >> their "classification" in Documentation/atomic_t.txt. >> >> Suggested-by: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com> >> Signed-off-by: Andrea Parri <parri.andrea@gmail.com> > > Reviewed-by: Boqun Feng <boqun.feng@gmail.com> > > I have a question below... > >> --- >> Changes since v2 [1]: >> - drop lk-rmw links >> >> Changes since v1 [2]: >> - add legenda/notations >> - add some SRCU, locking macros >> - update formatting of failure cases >> - update README file >> >> [1] https://lore.kernel.org/lkml/20240605134918.365579-1-parri.andrea@gmail.com/ >> [2] https://lore.kernel.org/lkml/20240524151356.236071-1-parri.andrea@gmail.com/ >> >> tools/memory-model/Documentation/README | 7 +- >> .../Documentation/herd-representation.txt | 106 ++++++++++++++++++ >> 2 files changed, 112 insertions(+), 1 deletion(-) >> create mode 100644 tools/memory-model/Documentation/herd-representation.txt >> >> diff --git a/tools/memory-model/Documentation/README b/tools/memory-model/Documentation/README >> index 304162743a5b8..44e7dae73b296 100644 >> --- a/tools/memory-model/Documentation/README >> +++ b/tools/memory-model/Documentation/README >> @@ -33,7 +33,8 @@ o You are familiar with Linux-kernel concurrency and the use of >> >> o You are familiar with Linux-kernel concurrency and the use >> of LKMM, and would like to learn about LKMM's requirements, >> - rationale, and implementation: explanation.txt >> + rationale, and implementation: explanation.txt and >> + herd-representation.txt >> >> o You are interested in the publications related to LKMM, including >> hardware manuals, academic literature, standards-committee >> @@ -61,6 +62,10 @@ control-dependencies.txt >> explanation.txt >> Detailed description of the memory model. >> >> +herd-representation.txt >> + The (abstract) representation of the Linux-kernel concurrency >> + primitives in terms of events. >> + >> litmus-tests.txt >> The format, features, capabilities, and limitations of the litmus >> tests that LKMM can evaluate. >> diff --git a/tools/memory-model/Documentation/herd-representation.txt b/tools/memory-model/Documentation/herd-representation.txt >> new file mode 100644 >> index 0000000000000..2fe270e902635 >> --- /dev/null >> +++ b/tools/memory-model/Documentation/herd-representation.txt >> @@ -0,0 +1,106 @@ >> +# >> +# Legenda: >> +# R, a Load event >> +# W, a Store event >> +# F, a Fence event >> +# LKR, a Lock-Read event >> +# LKW, a Lock-Write event >> +# UL, an Unlock event >> +# LF, a Lock-Fail event >> +# RL, a Read-Locked event >> +# RU, a Read-Unlocked event >> +# R*, a Load event included in RMW >> +# W*, a Store event included in RMW >> +# SRCU, a Sleepable-Read-Copy-Update event >> +# >> +# po, a Program-Order link >> +# rmw, a Read-Modify-Write link >> +# >> +# By convention, a blank entry/representation means "same as the preceding entry". >> +# >> + ------------------------------------------------------------------------------ >> + | C macro | Events | >> + ------------------------------------------------------------------------------ >> + | Non-RMW ops | | >> + ------------------------------------------------------------------------------ >> + | READ_ONCE | R[once] | >> + | atomic_read | | >> + | WRITE_ONCE | W[once] | >> + | atomic_set | | >> + | smp_load_acquire | R[acquire] | >> + | atomic_read_acquire | | >> + | smp_store_release | W[release] | >> + | atomic_set_release | | >> + | smp_store_mb | W[once] ->po F[mb] | >> + | smp_mb | F[mb] | >> + | smp_rmb | F[rmb] | >> + | smp_wmb | F[wmb] | >> + | smp_mb__before_atomic | F[before-atomic] | >> + | smp_mb__after_atomic | F[after-atomic] | >> + | spin_unlock | UL | >> + | spin_is_locked | On success: RL | >> + | | On failure: RU | >> + | smp_mb__after_spinlock | F[after-spinlock] | >> + | smp_mb__after_unlock_lock | F[after-unlock-lock] | >> + | rcu_read_lock | F[rcu-lock] | >> + | rcu_read_unlock | F[rcu-unlock] | >> + | synchronize_rcu | F[sync-rcu] | >> + | rcu_dereference | R[once] | >> + | rcu_assign_pointer | W[release] | >> + | srcu_read_lock | R[srcu-lock] | >> + | srcu_down_read | | >> + | srcu_read_unlock | W[srcu-unlock] | >> + | srcu_up_read | | >> + | synchronize_srcu | SRCU[sync-srcu] | >> + | smp_mb__after_srcu_read_unlock | F[after-srcu-read-unlock] | >> + ------------------------------------------------------------------------------ >> + | RMW ops w/o return value | | >> + ------------------------------------------------------------------------------ >> + | atomic_add | R*[noreturn] ->rmw W*[once] | >> + | 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] | > > Just to double check, there is also a ->po relation between R*[once] and > W*[once], right? It might not be important right now, but it's important > when we move to what Jonas is proposing: > > https://lore.kernel.org/lkml/20240604152922.495908-1-jonas.oberhauser@huaweicloud.com/ This follows from rmw \subset po. However, this might not be immediately clear for the reader so having it explicit is a good idea. Reviewed-by: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com> > > So just check with you ;-) Thanks! > > Regards, > Boqun > >> + | atomic_fetch_add | | >> + | atomic_fetch_and | | >> + | atomic_xchg | | >> + | xchg | | >> + | atomic_add_negative | | >> + | atomic_add_return_relaxed | R*[once] ->rmw W*[once] | >> + | atomic_fetch_add_relaxed | | >> + | atomic_fetch_and_relaxed | | >> + | atomic_xchg_relaxed | | >> + | xchg_relaxed | | >> + | atomic_add_negative_relaxed | | >> + | atomic_add_return_acquire | R*[acquire] ->rmw W*[once] | >> + | 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_fetch_add_release | | >> + | atomic_fetch_and_release | | >> + | atomic_xchg_release | | >> + | xchg_release | | >> + | atomic_add_negative_release | | >> + ------------------------------------------------------------------------------ >> + | Conditional RMW ops | | >> + ------------------------------------------------------------------------------ >> + | atomic_cmpxchg | On success: F[mb] ->po R*[once] | >> + | | ->rmw W*[once] ->po F[mb] | >> + | | On failure: R*[once] | >> + | 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] | >> + | spin_trylock | On success: LKR ->po LKW | >> + | | On failure: LF | >> + ------------------------------------------------------------------------------ >> -- >> 2.34.1 >>
> This follows from rmw \subset po. However, this might not be immediately > clear for the reader so having it explicit is a good idea. Sure. How about as follows: diff --git a/tools/memory-model/Documentation/herd-representation.txt b/tools/memory-model/Documentation/herd-representation.txt index 2fe270e902635..8255a2ff62e5f 100644 --- a/tools/memory-model/Documentation/herd-representation.txt +++ b/tools/memory-model/Documentation/herd-representation.txt @@ -14,7 +14,7 @@ # SRCU, a Sleepable-Read-Copy-Update event # # po, a Program-Order link -# rmw, a Read-Modify-Write link +# rmw, a Read-Modify-Write link; every rmw link is a po link # # By convention, a blank entry/representation means "same as the preceding entry". # I can respin the patch shortly to add something along these lines and the collected tags. Andrea
On 6/18/2024 11:54 AM, Andrea Parri wrote: >> This follows from rmw \subset po. However, this might not be immediately >> clear for the reader so having it explicit is a good idea. > > Sure. How about as follows: > > diff --git a/tools/memory-model/Documentation/herd-representation.txt b/tools/memory-model/Documentation/herd-representation.txt > index 2fe270e902635..8255a2ff62e5f 100644 > --- a/tools/memory-model/Documentation/herd-representation.txt > +++ b/tools/memory-model/Documentation/herd-representation.txt > @@ -14,7 +14,7 @@ > # SRCU, a Sleepable-Read-Copy-Update event > # > # po, a Program-Order link > -# rmw, a Read-Modify-Write link > +# rmw, a Read-Modify-Write link; every rmw link is a po link > # > # By convention, a blank entry/representation means "same as the preceding entry". > # > > I can respin the patch shortly to add something along these lines and > the collected tags. > > Andrea Sounds good to me. Hernan
> Just to double check, there is also a ->po relation between R*[once] and > W*[once], right? That's right. rmw = rmw & po I could add a note about that, but I would stick with the current patch /version (and your Reviewed-by:) unless other requests. Andrea
On Tue, Jun 18, 2024 at 05:27:45AM +0200, Andrea Parri wrote: > > Just to double check, there is also a ->po relation between R*[once] and > > W*[once], right? > > That's right. rmw = rmw & po > > I could add a note about that, but I would stick with the current patch > /version (and your Reviewed-by:) unless other requests. > Current version is fine to me, thanks! Regards, Boqun > Andrea
© 2016 - 2025 Red Hat, Inc.