| 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
| ||
|
Date: Tue, 18 Jun 2024 11:19:53 +0200 From: Hernan Ponce de Leon <hernan.poncedeleon@...weicloud.com> To: Boqun Feng <boqun.feng@...il.com>, 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, jonas.oberhauser@...weicloud.com Subject: Re: [PATCH v3] tools/memory-model: Document herd7 (abstract) representation 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@...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/ 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@...weicloud.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