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@xxxxxxxxxxxxxxx> Signed-off-by: Andrea Parri <parri.andrea@xxxxxxxxx> --- 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@xxxxxxxxx/ [2] https://lore.kernel.org/lkml/20240524151356.236071-1-parri.andrea@xxxxxxxxx/ 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.1
