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@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);