linux-kernel - Re: [RFC 3/3] tools/memory-model: Add litmus test for RMW + smp_mb__after

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

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Message-ID: <Pine.LNX.4.44L0.2002141049310.1579-100000@iolanthe.rowland.org>
Date:   Fri, 14 Feb 2020 10:58:57 -0500 (EST)
From:   Alan Stern <stern@...land.harvard.edu>
To:     Boqun Feng <boqun.feng@...il.com>
cc:     linux-kernel@...r.kernel.org,
        Andrea Parri <parri.andrea@...il.com>,
        Will Deacon <will@...nel.org>,
        Peter Zijlstra <peterz@...radead.org>,
        Nicholas Piggin <npiggin@...il.com>,
        David Howells <dhowells@...hat.com>,
        Jade Alglave <j.alglave@....ac.uk>,
        Luc Maranget <luc.maranget@...ia.fr>,
        "Paul E. McKenney" <paulmck@...nel.org>,
        Akira Yokosawa <akiyks@...il.com>,
        Daniel Lustig <dlustig@...dia.com>,
        Jonathan Corbet <corbet@....net>, <linux-arch@...r.kernel.org>,
        <linux-doc@...r.kernel.org>
Subject: Re: [RFC 3/3] tools/memory-model: Add litmus test for RMW +
 smp_mb__after_atomic()

On Fri, 14 Feb 2020, Boqun Feng wrote:

> We already use a litmus test in atomic_t.txt to describe atomic RMW +
> smp_mb__after_atomic() is "strong acquire" (both the read and the write
> part is ordered).

"strong acquire" is not an appropriate description -- there is no such
thing as a strong acquire in the LKMM -- nor is it a good name for the
litmus test.  A better description would be "stronger than acquire", as
in the sentence preceding the litmus test in atomic_t.txt.

>  So make it a litmus test in memory-model litmus-tests
> directory, so that people can access the litmus easily.
> 
> Additionally, change the processor numbers "P1, P2" to "P0, P1" in
> atomic_t.txt for the consistency with the processor numbers in the
> litmus test, which herd can handle.
> 
> Signed-off-by: Boqun Feng <boqun.feng@...il.com>
> ---
>  Documentation/atomic_t.txt                    |  6 ++--
>  ...+mb__after_atomic-is-strong-acquire.litmus | 29 +++++++++++++++++++
>  tools/memory-model/litmus-tests/README        |  5 ++++
>  3 files changed, 37 insertions(+), 3 deletions(-)
>  create mode 100644 tools/memory-model/litmus-tests/Atomic-RMW+mb__after_atomic-is-strong-acquire.litmus
> 
> diff --git a/Documentation/atomic_t.txt b/Documentation/atomic_t.txt
> index ceb85ada378e..e3ad4e4cd9ed 100644
> --- a/Documentation/atomic_t.txt
> +++ b/Documentation/atomic_t.txt
> @@ -238,14 +238,14 @@ strictly stronger than ACQUIRE. As illustrated:
>    {
>    }
>  
> -  P1(int *x, atomic_t *y)
> +  P0(int *x, atomic_t *y)
>    {
>      r0 = READ_ONCE(*x);
>      smp_rmb();
>      r1 = atomic_read(y);
>    }
>  
> -  P2(int *x, atomic_t *y)
> +  P1(int *x, atomic_t *y)
>    {
>      atomic_inc(y);
>      smp_mb__after_atomic();
> @@ -260,7 +260,7 @@ This should not happen; but a hypothetical atomic_inc_acquire() --
>  because it would not order the W part of the RMW against the following
>  WRITE_ONCE.  Thus:
>  
> -  P1			P2
> +  P0			P1
>  
>  			t = LL.acq *y (0)
>  			t++;
> diff --git a/tools/memory-model/litmus-tests/Atomic-RMW+mb__after_atomic-is-strong-acquire.litmus b/tools/memory-model/litmus-tests/Atomic-RMW+mb__after_atomic-is-strong-acquire.litmus
> new file mode 100644
> index 000000000000..e7216cf9d92a
> --- /dev/null
> +++ b/tools/memory-model/litmus-tests/Atomic-RMW+mb__after_atomic-is-strong-acquire.litmus
> @@ -0,0 +1,29 @@
> +C Atomic-RMW+mb__after_atomic-is-strong-acquire
> +
> +(*
> + * Result: Never
> + *
> + * Test of an atomic RMW followed by a smp_mb__after_atomic() is

s/Test of/Test that/

> + * "strong-acquire": both the read and write part of the RMW is ordered before

This should say "stronger than a normal acquire".  And "part" should be
"parts", and "is ordered" should be "are ordered".

Also, please try to arrange the line breaks so that the comment lines
don't have vastly different lengths.

Similar changes should be made for the text added to README.

Alan Stern