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

[Andrea Parri <parri.andrea@gmail.com>]

>  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