| 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: <1a3c892c-903e-8fd3-24a6-2454c2a55302@huaweicloud.com>
Date: Mon, 27 May 2024 14:22:47 +0200
From: Hernan Ponce de Leon <hernan.poncedeleon@...weicloud.com>
To: Andrea Parri <parri.andrea@...il.com>, stern@...land.harvard.edu,
will@...nel.org, peterz@...radead.org, boqun.feng@...il.com,
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
Cc: linux-kernel@...r.kernel.org, linux-arch@...r.kernel.org,
jonas.oberhauser@...weicloud.com
Subject: Re: [PATCH] tools/memory-model: Document herd7 (internal)
representation
On 5/24/2024 5:13 PM, 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 representation of synchronization 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>
> ---
> - Leaving srcu_{up,down}_read() and smp_mb__after_srcu_read_unlock() for
> the next version.
>
> - Limiting to "add" and "and" ops (skipping similar/same representations
> for "sub", "inc", "dec", "or", "xor", "andnot").
>
> - While preparing this submission, I recalled that atomic_add_unless()
> is not listed in the .def file. I can't remember the reason for this
> omission though.
>
> - While checking the information below using herd7, I've observed some
> "strange" behavior with spin_is_locked() (perhaps, unsurprisingly...);
> IAC, that's also excluded from this table/submission.
>
>
> .../Documentation/herd-representation.txt | 81 +++++++++++++++++++
> 1 file changed, 81 insertions(+)
> create mode 100644 tools/memory-model/Documentation/herd-representation.txt
>
> diff --git a/tools/memory-model/Documentation/herd-representation.txt b/tools/memory-model/Documentation/herd-representation.txt
> new file mode 100644
> index 0000000000000..94d0d0a9eee50
> --- /dev/null
> +++ b/tools/memory-model/Documentation/herd-representation.txt
> @@ -0,0 +1,81 @@
> + ---------------------------------------------------------------------------
> + | C macro | Events |
> + ---------------------------------------------------------------------------
> + | Non-RMW ops | |
> + ---------------------------------------------------------------------------
> + | READ_ONCE | R[once] |
> + | atomic_read | (as in the previous row) |
> + | 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] |
I expect this one to be hard-coded in herd7 source code, but I cannot
find it. Can you give me a pointer?
In fact, dartagnan uses W[Mb] ... another clear example of the need for
documentation as this one.
> + | 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 |
> + | 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_read_unlock | W[srcu-unlock] |
> + | synchronize_srcu | SRCU[sync-srcu] |
> + ---------------------------------------------------------------------------
> + | RMW ops w/o return value | |
> + ---------------------------------------------------------------------------
> + | atomic_add | R*[noreturn] ->rmw W*[once] |
> + | atomic_and | |
> + | spin_lock | LKR ->lk-rmw LKW |
What about spin_unlock?
> + ---------------------------------------------------------------------------
> + | 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 ->lk-rmw LKW |
> + | | On failure: LF |
> + ---------------------------------------------------------------------------
I found the extra spaces in the failure case very hard to read. Any
particular reason why you went with this format?
Hernan
Powered by blists - more mailing lists