| lists.openwall.net | lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC | |
|
Open Source and information security mailing list archives
| ||
|
Message-ID: <ZnC-cqQOEU2fd9tO@boqun-archlinux> Date: Mon, 17 Jun 2024 15:53:38 -0700 From: Boqun Feng <boqun.feng@...il.com> To: Andrea Parri <parri.andrea@...il.com> Cc: stern@...land.harvard.edu, will@...nel.org, peterz@...radead.org, npiggin@...il.com, dhowells@...hat.com, j.alglave@....ac.uk, luc.maranget@...ia.fr, paulmck@...nel.org, akiyks@...il.com, dlustig@...dia.com, joel@...lfernandes.org, linux-kernel@...r.kernel.org, linux-arch@...r.kernel.org, hernan.poncedeleon@...weicloud.com, jonas.oberhauser@...weicloud.com Subject: Re: [PATCH v3] tools/memory-model: Document herd7 (abstract) representation 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@...weicloud.com> > Signed-off-by: Andrea Parri <parri.andrea@...il.com> Reviewed-by: Boqun Feng <boqun.feng@...il.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 >
Powered by blists - more mailing lists