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

[Paul E. McKenney]

On Wed, Jun 05, 2024 at 10:47:03AM -0400, Alan Stern wrote:
> Paul:
> 
> Below is a new litmus test for the manual/locked directory in your 
> github archive.  It is based on a suggestion from Andrea Parri, and it 
> demonstrates a bug in the current LKMM lock.cat file.  Patches to fix 
> that file will be sent shortly.
> 
> Alan
> 
> ---
> 
> C islocked+lock+islocked+unlock+islocked.litmus
> 
> (*
>  * Result: Always
>  *
>  * This tests the memory model's implementation of spin_is_locked().
>  *)
> 
> {}
> 
> P0(spinlock_t *x)
> {
>         int r0;
> 	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)

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.
    
    Suggested-by: Andrea Parri <parri.andrea@xxxxxxxxx>
    Signed-off-by: Alan Stern <stern@xxxxxxxxxxxxxxxxxxx>
    Signed-off-by: Paul E. McKenney <paulmck@xxxxxxxxxx>

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
+
+(*
+ * Result: Always
+ *
+ * This tests the memory model's implementation of spin_is_locked().
+ *)
+
+{}
+
+P0(spinlock_t *x)
+{
+        int r0;
+	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)