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@xxxxxxxxxx>
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@xxxxxxxxx>
Signed-off-by: Paul E. McKenney <paulmck@xxxxxxxxxx>
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);
