[PATCH memory-model 1/3] Documentation/litmus-tests: Add locking tests to README

[PATCH memory-model 1/3] Documentation/litmus-tests: Add locking tests to README

[Paul E. McKenney]

This commit documents the litmus tests in the "locking" directory.

Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Cc: Alan Stern <stern@rowland.harvard.edu>
Cc: Will Deacon <will@kernel.org>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: Boqun Feng <boqun.feng@gmail.com>
Cc: Nicholas Piggin <npiggin@gmail.com>
Cc: David Howells <dhowells@redhat.com>
Cc: Jade Alglave <j.alglave@ucl.ac.uk>
Cc: Luc Maranget <luc.maranget@inria.fr>
Cc: "Paul E. McKenney" <paulmck@kernel.org>
Cc: Akira Yokosawa <akiyks@gmail.com>
Cc: Daniel Lustig <dlustig@nvidia.com>
Cc: Joel Fernandes <joel@joelfernandes.org>
Cc: Mark Rutland <mark.rutland@arm.com>
Cc: Jonathan Corbet <corbet@lwn.net>
Cc: <linux-arch@vger.kernel.org>
Cc: <linux-doc@vger.kernel.org>
---
 Documentation/litmus-tests/README | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)

diff --git a/Documentation/litmus-tests/README b/Documentation/litmus-tests/README
index 658d37860d397..5c8915e6fb684 100644
--- a/Documentation/litmus-tests/README
+++ b/Documentation/litmus-tests/README
@@ -22,6 +22,35 @@ Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
     NOTE: Require herd7 7.56 or later which supports "(void)expr".
 
 
+locking (/locking directory)
+----------------------------
+
+DCL-broken.litmus
+	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.
+
+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.
+
+	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.
+
+
 RCU (/rcu directory)
 --------------------
 
-- 
2.40.1

[PATCH memory-model 2/3] Documentation/litmus-tests: Demonstrate unordered failing cmpxchg

[Paul E. McKenney]

This commit adds four litmus tests showing that a failing cmpxchg()
operation is unordered unless followed by an smp_mb__after_atomic()
operation.

Suggested-by: Frederic Weisbecker <frederic@kernel.org>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Cc: Alan Stern <stern@rowland.harvard.edu>
Cc: Will Deacon <will@kernel.org>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: Boqun Feng <boqun.feng@gmail.com>
Cc: Nicholas Piggin <npiggin@gmail.com>
Cc: David Howells <dhowells@redhat.com>
Cc: Jade Alglave <j.alglave@ucl.ac.uk>
Cc: Luc Maranget <luc.maranget@inria.fr>
Cc: "Paul E. McKenney" <paulmck@kernel.org>
Cc: Akira Yokosawa <akiyks@gmail.com>
Cc: Daniel Lustig <dlustig@nvidia.com>
Cc: Joel Fernandes <joel@joelfernandes.org>
Cc: Mark Rutland <mark.rutland@arm.com>
Cc: Jonathan Corbet <corbet@lwn.net>
Cc: <linux-arch@vger.kernel.org>
Cc: <linux-doc@vger.kernel.org>
---
 Documentation/litmus-tests/README             | 48 ++++++++++++-------
 .../atomic/cmpxchg-fail-ordered-1.litmus      | 34 +++++++++++++
 .../atomic/cmpxchg-fail-ordered-2.litmus      | 30 ++++++++++++
 .../atomic/cmpxchg-fail-unordered-1.litmus    | 33 +++++++++++++
 .../atomic/cmpxchg-fail-unordered-2.litmus    | 30 ++++++++++++
 5 files changed, 159 insertions(+), 16 deletions(-)
 create mode 100644 Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-1.litmus
 create mode 100644 Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-2.litmus
 create mode 100644 Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-1.litmus
 create mode 100644 Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-2.litmus

diff --git a/Documentation/litmus-tests/README b/Documentation/litmus-tests/README
index 5c8915e6fb684..6c666f3422ea3 100644
--- a/Documentation/litmus-tests/README
+++ b/Documentation/litmus-tests/README
@@ -21,34 +21,50 @@ Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
     Test that atomic_set() cannot break the atomicity of atomic RMWs.
     NOTE: Require herd7 7.56 or later which supports "(void)expr".
 
+cmpxchg-fail-ordered-1.litmus
+    Demonstrate that a failing cmpxchg() operation acts as a full barrier
+    when followed by smp_mb__after_atomic().
+
+cmpxchg-fail-ordered-2.litmus
+    Demonstrate that a failing cmpxchg() operation acts as an acquire
+    operation when followed by smp_mb__after_atomic().
+
+cmpxchg-fail-unordered-1.litmus
+    Demonstrate that a failing cmpxchg() operation does not act as a
+    full barrier.
+
+cmpxchg-fail-unordered-2.litmus
+    Demonstrate that a failing cmpxchg() operation does not act as an
+    acquire operation.
+
 
 locking (/locking directory)
 ----------------------------
 
 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.
 
 
 RCU (/rcu directory)
diff --git a/Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-1.litmus b/Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-1.litmus
new file mode 100644
index 0000000000000..3df1d140b189b
--- /dev/null
+++ b/Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-1.litmus
@@ -0,0 +1,34 @@
+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);
+	smp_mb__after_atomic();
+	r0 = READ_ONCE(*x);
+}
+
+locations[0:r1;1:r1]
+exists (0:r0=0 /\ 1:r0=0)
diff --git a/Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-2.litmus b/Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-2.litmus
new file mode 100644
index 0000000000000..54146044a16f6
--- /dev/null
+++ b/Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-2.litmus
@@ -0,0 +1,30 @@
+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);
+}
+
+exists (0:r1=0 /\ 1:r1=1 /\ 1:r2=0)
diff --git a/Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-1.litmus b/Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-1.litmus
new file mode 100644
index 0000000000000..a727ce23b1a6e
--- /dev/null
+++ b/Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-1.litmus
@@ -0,0 +1,33 @@
+C cmpxchg-fail-unordered-1
+
+(*
+ * Result: Sometimes
+ *
+ * Demonstrate that a failing cmpxchg() operation does not act as a
+ * full barrier.  (In contrast, a successful cmpxchg() does act as a
+ * full barrier.)
+ *)
+
+{}
+
+P0(int *x, int *y, int *z)
+{
+	int r0;
+	int r1;
+
+	WRITE_ONCE(*x, 1);
+	r1 = cmpxchg(z, 1, 0);
+	r0 = READ_ONCE(*y);
+}
+
+P1(int *x, int *y, int *z)
+{
+	int r0;
+
+	WRITE_ONCE(*y, 1);
+	r1 = cmpxchg(z, 1, 0);
+	r0 = READ_ONCE(*x);
+}
+
+locations[0:r1;1:r1]
+exists (0:r0=0 /\ 1:r0=0)
diff --git a/Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-2.litmus b/Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-2.litmus
new file mode 100644
index 0000000000000..a245bac55b578
--- /dev/null
+++ b/Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-2.litmus
@@ -0,0 +1,30 @@
+C cmpxchg-fail-unordered-2
+
+(*
+ * Result: Sometimes
+ *
+ * Demonstrate that a failing cmpxchg() operation does not act as either
+ * an acquire release operation.  (In contrast, a successful cmpxchg()
+ * does act as both an acquire and a release operation.)
+ *)
+
+{}
+
+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);
+	r2 = READ_ONCE(*x);
+}
+
+exists (0:r1=0 /\ 1:r1=1 /\ 1:r2=0)
-- 
2.40.1

Re: [PATCH memory-model 2/3] Documentation/litmus-tests: Demonstrate unordered failing cmpxchg

[Andrea Parri]

>  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

Re: [PATCH memory-model 2/3] Documentation/litmus-tests: Demonstrate unordered failing cmpxchg

[Paul E. McKenney]

On Fri, Apr 05, 2024 at 12:05:11PM +0200, Andrea Parri wrote:
> >  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?

Good eyes!  I will catch this in my next rebase.

> > +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.

Good catch in all four tests, thank you!

Does the patch shown at the end of this email clear things up for you?

							Thanx, Paul

> > +	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

------------------------------------------------------------------------

commit 5ce4d0efe11fd101ff938f6116cdd9b6fe46a98c
Author: Paul E. McKenney <paulmck@kernel.org>
Date:   Mon Apr 8 13:41:22 2024 -0700

    Documentation/litmus-tests: Make cmpxchg() tests safe for klitmus
    
    The four litmus tests in Documentation/litmus-tests/atomic do not
    declare all of their local variables.  Although this is just fine for LKMM
    analysis by herd7, it causes build failures when run in-kernel by klitmus.
    This commit therefore adjusts these tests to declare all local variables.
    
    Reported-by: Andrea Parri <parri.andrea@gmail.com>
    Signed-off-by: Paul E. McKenney <paulmck@kernel.org>

diff --git a/Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-1.litmus b/Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-1.litmus
index 3df1d140b189b..c0f93dc07105e 100644
--- a/Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-1.litmus
+++ b/Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-1.litmus
@@ -23,6 +23,7 @@ P0(int *x, int *y, int *z)
 P1(int *x, int *y, int *z)
 {
 	int r0;
+	int r1;
 
 	WRITE_ONCE(*y, 1);
 	r1 = cmpxchg(z, 1, 0);
diff --git a/Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-2.litmus b/Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-2.litmus
index 54146044a16f6..5c06054f46947 100644
--- a/Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-2.litmus
+++ b/Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-2.litmus
@@ -11,7 +11,6 @@ C cmpxchg-fail-ordered-2
 
 P0(int *x, int *y)
 {
-	int r0;
 	int r1;
 
 	WRITE_ONCE(*x, 1);
@@ -20,7 +19,8 @@ P0(int *x, int *y)
 
 P1(int *x, int *y)
 {
-	int r0;
+	int r1;
+	int r2;
 
 	r1 = cmpxchg(y, 0, 1);
 	smp_mb__after_atomic();
diff --git a/Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-1.litmus b/Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-1.litmus
index a727ce23b1a6e..39ea1f56a28d2 100644
--- a/Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-1.litmus
+++ b/Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-1.litmus
@@ -23,6 +23,7 @@ P0(int *x, int *y, int *z)
 P1(int *x, int *y, int *z)
 {
 	int r0;
+	int r1;
 
 	WRITE_ONCE(*y, 1);
 	r1 = cmpxchg(z, 1, 0);
diff --git a/Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-2.litmus b/Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-2.litmus
index a245bac55b578..61aab24a4a643 100644
--- a/Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-2.litmus
+++ b/Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-2.litmus
@@ -12,7 +12,6 @@ C cmpxchg-fail-unordered-2
 
 P0(int *x, int *y)
 {
-	int r0;
 	int r1;
 
 	WRITE_ONCE(*x, 1);
@@ -21,7 +20,8 @@ P0(int *x, int *y)
 
 P1(int *x, int *y)
 {
-	int r0;
+	int r1;
+	int r2;
 
 	r1 = cmpxchg(y, 0, 1);
 	r2 = READ_ONCE(*x);

Re: [PATCH memory-model 2/3] Documentation/litmus-tests: Demonstrate unordered failing cmpxchg

[Andrea Parri]

> Good catch in all four tests, thank you!
> 
> Does the patch shown at the end of this email clear things up for you?

Yes, that'll do it.

  Andrea

[PATCH memory-model 3/3] Documentation/atomic_t: Emphasize that failed atomic operations give no ordering

[Paul E. McKenney]

The ORDERING section of Documentation/atomic_t.txt can easily be read as
saying that conditional atomic RMW operations that fail are ordered when
those operations have the _acquire() or _release() suffixes.  This is
not the case, therefore update this section to make it clear that failed
conditional atomic RMW operations provide no ordering.

Reported-by: Anna-Maria Behnsen <anna-maria@linutronix.de>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Cc: Alan Stern <stern@rowland.harvard.edu>
Cc: Will Deacon <will@kernel.org>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: Boqun Feng <boqun.feng@gmail.com>
Cc: Nicholas Piggin <npiggin@gmail.com>
Cc: David Howells <dhowells@redhat.com>
Cc: Jade Alglave <j.alglave@ucl.ac.uk>
Cc: Luc Maranget <luc.maranget@inria.fr>
Cc: "Paul E. McKenney" <paulmck@kernel.org>
Cc: Akira Yokosawa <akiyks@gmail.com>
Cc: Daniel Lustig <dlustig@nvidia.com>
Cc: Joel Fernandes <joel@joelfernandes.org>
Cc: Mark Rutland <mark.rutland@arm.com>
Cc: Jonathan Corbet <corbet@lwn.net>
Cc: <linux-arch@vger.kernel.org>
Cc: <linux-doc@vger.kernel.org>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
Acked-by: Mark Rutland <mark.rutland@arm.com>
---
 Documentation/atomic_t.txt | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Documentation/atomic_t.txt b/Documentation/atomic_t.txt
index d7adc6d543db4..bee3b1bca9a7b 100644
--- a/Documentation/atomic_t.txt
+++ b/Documentation/atomic_t.txt
@@ -171,14 +171,14 @@ The rule of thumb:
  - RMW operations that are conditional are unordered on FAILURE,
    otherwise the above rules apply.
 
-Except of course when an operation has an explicit ordering like:
+Except of course when a successful operation has an explicit ordering like:
 
  {}_relaxed: unordered
  {}_acquire: the R of the RMW (or atomic_read) is an ACQUIRE
  {}_release: the W of the RMW (or atomic_set)  is a  RELEASE
 
 Where 'unordered' is against other memory locations. Address dependencies are
-not defeated.
+not defeated.  Conditional operations are still unordered on FAILURE.
 
 Fully ordered primitives are ordered against everything prior and everything
 subsequent. Therefore a fully ordered primitive is like having an smp_mb()
-- 
2.40.1