Received-SPF: pass (google.com: domain of linux-kernel+bounces-172580-linux.lists.archive=gmail.com@vger.kernel.org designates 2604:1380:45d1:ec00::1 as permitted sender) client-ip=2604:1380:45d1:ec00::1;
Date: Wed, 8 May 2024 03:17:15 +0200
From: Andrea Parri <parri.andrea@gmail.com>
To: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
Cc: Alan Stern <stern@rowland.harvard.edu>,
	"Paul E. McKenney" <paulmck@kernel.org>,
	linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org,
	kernel-team@meta.com, mingo@kernel.org, will@kernel.org,
	peterz@infradead.org, boqun.feng@gmail.com, npiggin@gmail.com,
	dhowells@redhat.com, j.alglave@ucl.ac.uk, luc.maranget@inria.fr,
	akiyks@gmail.com, Frederic Weisbecker <frederic@kernel.org>,
	Daniel Lustig <dlustig@nvidia.com>,
	Joel Fernandes <joel@joelfernandes.org>,
	Mark Rutland <mark.rutland@arm.com>,
	Jonathan Corbet <corbet@lwn.net>, linux-doc@vger.kernel.org
Subject: Re: [PATCH memory-model 2/4] Documentation/litmus-tests: Demonstrate
 unordered failing cmpxchg
Message-ID: <ZjrSm119+IfIU9eU@andrea>
References: <42a43181-a431-44bd-8aff-6b305f8111ba@paulmck-laptop>
 <20240501232132.1785861-2-paulmck@kernel.org>
 <c97f0529-5a8f-4a82-8e14-0078d4372bdc@huaweicloud.com>
 <16381d02-cb70-4ae5-b24e-aa73afad9aed@huaweicloud.com>
 <2a695f63-6c9a-4837-ac03-f0a5c63daaaf@paulmck-laptop>
 <c168f56f-dfae-4cac-bc61-fc5a93ee3aed@rowland.harvard.edu>
 <fd2369ed-1e84-4e44-ac80-cd316f8e7051@huaweicloud.com>
Precedence: bulk
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <fd2369ed-1e84-4e44-ac80-cd316f8e7051@huaweicloud.com>

> > Don't the annotations in linux-kernel.def and linux-kernel.bell (like
> > "noreturn") already make this explicit?
> 
> Not that I'm aware. All I can see there is that according to .bell RMW don't
> have an mb mode, but according to .def they do.
> 
> How this mb disappears between parsing the code (.def) and interpreting it
> (.bell) is totally implicit. Including how noreturn affects this
> disappeareance.

IIRC, that's more or less implicit  ;-) in the herd macros of the .def file;
for example,


  (noreturn)

  - atomic_add(V,X) { __atomic_op(X,+,V); }

    Generates a pair of R*[noreturn] and W*[once] events


  (w/ return)

  - atomic_add_return_relaxed(V,X) __atomic_op_return{once}(X,+,V)

    Generates a pair of R*[once] and W*[once] events

  - atomic_add_return_acquire(V,X) __atomic_op_return{acquire}(X,+,V)

    Generates a pair of R*[acquire] and W*[once] events

  - atomic_add_return_release(V,X) __atomic_op_return{acquire}(X,+,V)

    Generates a pair of R*[once] and W*[release] events

  - atomic_add_return(V,X) __atomic_op_return{mb}(X,+,V)

    Generates a pair of R*[once] and W*[once] events plus two F[mb] events


  (possibly failing)

  - atomic_cmpxchg_relaxed(X,V,W) __cmpxchg{once}(X,V,W)

    Generates a pair of R*[once] and W*[once] events if successful;
    a single R*[once] event otherwise.

  - atomic_cmpxchg_acquire(X,V,W) __cmpxchg{acquire}(X,V,W)

    Generates a pair of R*[acquire] and W*[once] events if successful;
    a single R*[once] event otherwise.

  - atomic_cmpxchg_release(X,V,W) __cmpxchg{release}(X,V,W)

    Generates a pair of R*[once] and W*[release] events if successful;
    a single R*[once] event otherwise.

  - atomic_cmpxchg(X,V,W) __cmpxchg{mb}(X,V,W)

    Generates a pair of R*[once] and W*[once] events plus two F[mb] events
    if successful; a single R*[once] event otherwise.


The line

  instructions RMW[{'once,'acquire,'release}]

in the .bell file seems to be effectively redundant (perhaps a LISA backward
-compatibility?): consider

  $ cat rmw.litmus
  C rmw
    
  {}
    
  P0(atomic_t *x)
  {
	int r0;

	r0 = atomic_inc_return_release(x);
  }

  exists (x=1)

Some experiments:

  - Upon removing 'release from "(instructions) RMW"

    $ herd7 -conf linux-kernel.cfg rmw.litmus 
    Test rmw Allowed
    States 1
    [x]=1;
    Ok
    Witnesses
    Positive: 1 Negative: 0
    Condition exists ([x]=1)
    Observation rmw Always 1 0
    Time rmw 0.00
    Hash=3a2dd354c250206d993d31f05f3f595c

  - Upon restoring 'release in RMW and removing it from W

    $ herd7 -conf linux-kernel.cfg rmw.litmus 
    Test rmw Allowed
    States 1
    [x]=1;
    Ok
    Witnesses
    Positive: 1 Negative: 0
    Condition exists ([x]=1)
    Observation rmw Always 1 0
    Time rmw 0.00
    Hash=3a2dd354c250206d993d31f05f3f595c

  - Upon removing 'release from both W and RMW

    $ herd7 -conf linux-kernel.cfg rmw.litmus (herd complains... )
    File "./linux-kernel.bell", line 76, characters 32-39: unbound var: Release

But I'd have to defer to Luc/Jade about herd internals and/or recommended style
on this matter.

  Andrea