Re: New locking test for the paulmckrcu/litmus github archive

[Alan Stern]

On Wed, Jun 05, 2024 at 11:25:11AM -0700, Paul E. McKenney wrote:
> Thank you both!
> 
> I queued and pushed the following commit, please let me know if it
> needs adjustment.
> 
> 							Thanx, Paul
> 
> ------------------------------------------------------------------------
> 
> commit fb65813a7a181cd86c50bb03f9df1f6a398fa22b
> Author: Alan Stern <stern@xxxxxxxxxxxxxxxxxxx>
> Date:   Wed Jun 5 11:20:47 2024 -0700
> 
>     manual/locked: Add single-threaded spin_is_locked() test
>     
>     This new litmus test demonstrates a bug in the current LKMM lock.cat file.
>     This bug results in the following output:
>     
>             Test CoWWW+sil-lock-sil-unlock-sil Allowed
>             States 0
>             No
>             Witnesses
>             Positive: 0 Negative: 0
>             Condition exists (0:r0=0 /\ 0:r1=1 /\ 0:r2=0)
>             Observation CoWWW+sil-lock-sil-unlock-sil Never 0 0
>             Time CoWWW+sil-lock-sil-unlock-sil 0.01
>             Hash=cf12d53b4d1afec2e46bf9886af219c8
>     
>     This is consistent with a deadlock.  After the fix, there should be one
>     execution that matches the "exists" clause, hence an "Always" result.

The part about being consistent with a deadlock is not very important; 
I'd omit it.  Also, the second sentence is ambiguous; change it to:

	After the fix, there should be one execution that matches the 
	"exists" clause and no executions that don't match, hence an 
	"Always" result.

> diff --git a/manual/locked/CoWWW+sil-lock-sil-unlock-sil.litmus b/manual/locked/CoWWW+sil-lock-sil-unlock-sil.litmus
> new file mode 100644
> index 00000000..cee5abf4
> --- /dev/null
> +++ b/manual/locked/CoWWW+sil-lock-sil-unlock-sil.litmus
> @@ -0,0 +1,24 @@
> +C CoWWW+sil-lock-sil-unlock-sil.litmus

Where does the "CoWWW" part of the name come from?  If it refers to 
coherence order and three writes, I'll point out that the litmus test 
contains only two writes -- which would better be described as a lock 
and an unlock.  (Or are you counting the "write" that sets the lock's 
initial value?)

> +
> +(*
> + * Result: Always
> + *
> + * This tests the memory model's implementation of spin_is_locked().
> + *)
> +
> +{}
> +
> +P0(spinlock_t *x)
> +{
> +        int r0;

Oops!  Apparently I managed not to convert the spaces on that line to a 
tab.  Can you take care of that?

Alan

> +	int r1;
> +	int r2;
> +
> +	r0 = spin_is_locked(x);
> +	spin_lock(x);
> +	r1 = spin_is_locked(x);
> +	spin_unlock(x);
> +	r2 = spin_is_locked(x);
> +}
> +
> +exists (0:r0=0 /\ 0:r1=1 /\ 0:r2=0)