On Wed, Jun 19, 2024 at 03:06:04AM +0200, Andrea Parri wrote: > 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@xxxxxxxxxxxxxxx> > Signed-off-by: Andrea Parri <parri.andrea@xxxxxxxxx> > Reviewed-by: Boqun Feng <boqun.feng@xxxxxxxxx> > Reviewed-by: Hernan Ponce de Leon <hernan.poncedeleon@xxxxxxxxxxxxxxx> I have reverted the previous version and queued this one, thank you!!! Thanx, Paul > --- > Changes since v3 [1]: > - note that rmw is a subset of po > - include paulmck's wordsmithing > - add limitations, aka stress that certain ops have been intentionally omitted > - add collected Reviewed-by: tags > > Changes since v2 [2]: > - drop lk-rmw links > > Changes since v1 [3]: > - add legenda/notations > - add some SRCU, locking macros > - update formatting of failure cases > - update README file > > [1] https://lore.kernel.org/lkml/20240617201759.1670994-1-parri.andrea@xxxxxxxxx/ > [2] https://lore.kernel.org/lkml/20240605134918.365579-1-parri.andrea@xxxxxxxxx/ > [3] https://lore.kernel.org/lkml/20240524151356.236071-1-parri.andrea@xxxxxxxxx/ > > tools/memory-model/Documentation/README | 7 +- > .../Documentation/herd-representation.txt | 110 ++++++++++++++++++ > 2 files changed, 116 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 db90a26dbdf40..1f73014cc48a3 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 > @@ -57,6 +58,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..ed988906f2b71 > --- /dev/null > +++ b/tools/memory-model/Documentation/herd-representation.txt > @@ -0,0 +1,110 @@ > +# > +# 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 - every rmw link is a po link > +# > +# By convention, a blank line in a cell means "same as the preceding line". > +# > +# Disclaimer. The table includes representations of "add" and "and" operations; > +# corresponding/identical representations of "sub", "inc", "dec" and "or", "xor", > +# "andnot" operations are omitted. > +# > + ------------------------------------------------------------------------------ > + | 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.1 >
