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> 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
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);
© 2016 - 2026 Red Hat, Inc.