Hello!
This series contains LKMM documentation updates:
1. Documentation/litmus-tests: Add locking tests to README.
2. Documentation/litmus-tests: Demonstrate unordered failing cmpxchg.
3. Documentation/atomic_t: Emphasize that failed atomic operations
give no ordering.
Thanx, Paul
------------------------------------------------------------------------
Documentation/litmus-tests/README | 48 ++++++----
b/Documentation/atomic_t.txt | 4
b/Documentation/litmus-tests/README | 29 ++++++
b/Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-1.litmus | 34 +++++++
b/Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-2.litmus | 30 ++++++
b/Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-1.litmus | 33 ++++++
b/Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-2.litmus | 30 ++++++
7 files changed, 190 insertions(+), 18 deletions(-)
Hello!
This series contains LKMM documentation updates:
1. Documentation/litmus-tests: Add locking tests to README.
2. Documentation/litmus-tests: Demonstrate unordered failing cmpxchg.
3. Documentation/atomic_t: Emphasize that failed atomic operations
give no ordering.
4. Documentation/litmus-tests: Make cmpxchg() tests safe for klitmus.
Changes since V1:
o Apply formatting feedback from Andrea Parri
o Add patch 4 that makes tests safe for klitmus, also based on
feedback from Andrea Parri.
Thanx, Paul
------------------------------------------------------------------------
Documentation/litmus-tests/README | 16 ++++
Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-1.litmus | 1
Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-2.litmus | 4 -
Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-1.litmus | 1
Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-2.litmus | 4 -
b/Documentation/atomic_t.txt | 4 -
b/Documentation/litmus-tests/README | 29 ++++++++
b/Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-1.litmus | 34 ++++++++++
b/Documentation/litmus-tests/atomic/cmpxchg-fail-ordered-2.litmus | 30 ++++++++
b/Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-1.litmus | 33 +++++++++
b/Documentation/litmus-tests/atomic/cmpxchg-fail-unordered-2.litmus | 30 ++++++++
11 files changed, 180 insertions(+), 6 deletions(-)
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 <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
---
.../litmus-tests/atomic/cmpxchg-fail-ordered-1.litmus | 1 +
.../litmus-tests/atomic/cmpxchg-fail-ordered-2.litmus | 4 ++--
.../litmus-tests/atomic/cmpxchg-fail-unordered-1.litmus | 1 +
.../litmus-tests/atomic/cmpxchg-fail-unordered-2.litmus | 4 ++--
4 files changed, 6 insertions(+), 4 deletions(-)
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);
--
2.40.1
This commit documents the litmus tests in the "locking" directory.
[ paulmck: Apply formatting feedback from Andrea Parri. ]
Signed-off-by: Paul E. McKenney <[email protected]>
Cc: Alan Stern <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Boqun Feng <[email protected]>
Cc: Nicholas Piggin <[email protected]>
Cc: David Howells <[email protected]>
Cc: Jade Alglave <[email protected]>
Cc: Luc Maranget <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Akira Yokosawa <[email protected]>
Cc: Daniel Lustig <[email protected]>
Cc: Joel Fernandes <[email protected]>
Cc: Mark Rutland <[email protected]>
Cc: Jonathan Corbet <[email protected]>
Cc: <[email protected]>
Cc: <[email protected]>
---
Documentation/litmus-tests/README | 29 +++++++++++++++++++++++++++++
1 file changed, 29 insertions(+)
diff --git a/Documentation/litmus-tests/README b/Documentation/litmus-tests/README
index 658d37860d397..26ca56df02125 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
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 <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
Cc: Alan Stern <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Boqun Feng <[email protected]>
Cc: Nicholas Piggin <[email protected]>
Cc: David Howells <[email protected]>
Cc: Jade Alglave <[email protected]>
Cc: Luc Maranget <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Akira Yokosawa <[email protected]>
Cc: Daniel Lustig <[email protected]>
Cc: Joel Fernandes <[email protected]>
Cc: Mark Rutland <[email protected]>
Cc: Jonathan Corbet <[email protected]>
Cc: <[email protected]>
Cc: <[email protected]>
Acked-by: Andrea Parri <[email protected]>
Acked-by: Mark Rutland <[email protected]>
---
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
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 <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
Cc: Alan Stern <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Boqun Feng <[email protected]>
Cc: Nicholas Piggin <[email protected]>
Cc: David Howells <[email protected]>
Cc: Jade Alglave <[email protected]>
Cc: Luc Maranget <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Akira Yokosawa <[email protected]>
Cc: Daniel Lustig <[email protected]>
Cc: Joel Fernandes <[email protected]>
Cc: Mark Rutland <[email protected]>
Cc: Jonathan Corbet <[email protected]>
Cc: <[email protected]>
Cc: <[email protected]>
---
Documentation/litmus-tests/README | 16 +++++++++
.../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, 143 insertions(+)
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 26ca56df02125..6c666f3422ea3 100644
--- a/Documentation/litmus-tests/README
+++ b/Documentation/litmus-tests/README
@@ -21,6 +21,22 @@ 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)
----------------------------
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
> This series contains LKMM documentation updates:
>
> 1. Documentation/litmus-tests: Add locking tests to README.
>
> 2. Documentation/litmus-tests: Demonstrate unordered failing cmpxchg.
>
> 3. Documentation/atomic_t: Emphasize that failed atomic operations
> give no ordering.
>
> 4. Documentation/litmus-tests: Make cmpxchg() tests safe for klitmus.
For the series,
Acked-by: Andrea Parri <[email protected]>
Andrea
On Thu, May 02, 2024 at 11:36:51AM +0200, Andrea Parri wrote:
> > This series contains LKMM documentation updates:
> >
> > 1. Documentation/litmus-tests: Add locking tests to README.
> >
> > 2. Documentation/litmus-tests: Demonstrate unordered failing cmpxchg.
> >
> > 3. Documentation/atomic_t: Emphasize that failed atomic operations
> > give no ordering.
> >
> > 4. Documentation/litmus-tests: Make cmpxchg() tests safe for klitmus.
>
> For the series,
>
> Acked-by: Andrea Parri <[email protected]>
Thank you! I will apply on my next rebase.
Thanx, Paul