Received-SPF: pass (google.com: domain of linux-kernel+bounces-132789-linux.lists.archive=gmail.com@vger.kernel.org designates 2604:1380:4601:e00::3 as permitted sender) client-ip=2604:1380:4601:e00::3;
Date: Fri, 5 Apr 2024 12:05:11 +0200
From: Andrea Parri <parri.andrea@gmail.com>
To: "Paul E. McKenney" <paulmck@kernel.org>
Cc: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org,
	kernel-team@meta.com, mingo@kernel.org, stern@rowland.harvard.edu,
	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/3] Documentation/litmus-tests: Demonstrate
 unordered failing cmpxchg
Message-ID: <Zg/M141yzwnwPbCi@andrea>
References: <8550daf1-4bfd-4607-8325-bfb7c1e2d8c7@paulmck-laptop>
 <20240404192649.531112-2-paulmck@kernel.org>
Precedence: bulk
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <20240404192649.531112-2-paulmck@kernel.org>

>  DCL-broken.litmus
> -	Demonstrates that double-checked locking needs more than just
> -	the obvious lock acquisitions and releases.
> +    Demonstrates that double-checked locking needs more than just
> +    the obvious lock acquisitions and releases.
>  
>  DCL-fixed.litmus
> -	Demonstrates corrected double-checked locking that uses
> -	smp_store_release() and smp_load_acquire() in addition to the
> -	obvious lock acquisitions and releases.
> +    Demonstrates corrected double-checked locking that uses
> +    smp_store_release() and smp_load_acquire() in addition to the
> +    obvious lock acquisitions and releases.
>  
>  RM-broken.litmus
> -	Demonstrates problems with "roach motel" locking, where code is
> -	freely moved into lock-based critical sections.  This example also
> -	shows how to use the "filter" clause to discard executions that
> -	would be excluded by other code not modeled in the litmus test.
> -	Note also that this "roach motel" optimization is emulated by
> -	physically moving P1()'s two reads from x under the lock.
> +    Demonstrates problems with "roach motel" locking, where code is
> +    freely moved into lock-based critical sections.  This example also
> +    shows how to use the "filter" clause to discard executions that
> +    would be excluded by other code not modeled in the litmus test.
> +    Note also that this "roach motel" optimization is emulated by
> +    physically moving P1()'s two reads from x under the lock.
>  
> -	What is a roach motel?	This is from an old advertisement for
> -	a cockroach trap, much later featured in one of the "Men in
> -	Black" movies.	"The roaches check in.	They don't check out."
> +    What is a roach motel?  This is from an old advertisement for
> +    a cockroach trap, much later featured in one of the "Men in
> +    Black" movies.  "The roaches check in.  They don't check out."
>  
>  RM-fixed.litmus
> -	The counterpart to RM-broken.litmus, showing P0()'s two loads from
> -	x safely outside of the critical section.
> +    The counterpart to RM-broken.litmus, showing P0()'s two loads from
> +    x safely outside of the critical section.

AFAIU, the changes above belong to patch #1.  Looks like you realigned
the text, but forgot to integrate the changes in #1?


> +C cmpxchg-fail-ordered-1
> +
> +(*
> + * Result: Never
> + *
> + * Demonstrate that a failing cmpxchg() operation will act as a full
> + * barrier when followed by smp_mb__after_atomic().
> + *)
> +
> +{}
> +
> +P0(int *x, int *y, int *z)
> +{
> +	int r0;
> +	int r1;
> +
> +	WRITE_ONCE(*x, 1);
> +	r1 = cmpxchg(z, 1, 0);
> +	smp_mb__after_atomic();
> +	r0 = READ_ONCE(*y);
> +}
> +
> +P1(int *x, int *y, int *z)
> +{
> +	int r0;
> +
> +	WRITE_ONCE(*y, 1);
> +	r1 = cmpxchg(z, 1, 0);

P1's r1 is undeclared (so klitmus7 will complain).

The same observation holds for cmpxchg-fail-unordered-1.litmus.


> +	smp_mb__after_atomic();
> +	r0 = READ_ONCE(*x);
> +}
> +
> +locations[0:r1;1:r1]
> +exists (0:r0=0 /\ 1:r0=0)


> +C cmpxchg-fail-ordered-2
> +
> +(*
> + * Result: Never
> + *
> + * Demonstrate use of smp_mb__after_atomic() to make a failing cmpxchg
> + * operation have acquire ordering.
> + *)
> +
> +{}
> +
> +P0(int *x, int *y)
> +{
> +	int r0;
> +	int r1;
> +
> +	WRITE_ONCE(*x, 1);
> +	r1 = cmpxchg(y, 0, 1);
> +}
> +
> +P1(int *x, int *y)
> +{
> +	int r0;
> +
> +	r1 = cmpxchg(y, 0, 1);
> +	smp_mb__after_atomic();
> +	r2 = READ_ONCE(*x);

P1's r1 and r2 are undeclared.  P0's r0 and P1's r0 are unused.

Same for cmpxchg-fail-unordered-2.litmus.

  Andrea