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

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Date: Wed, 5 Jun 2024 11:25:11 -0700
From: "Paul E. McKenney" <paulmck@...nel.org>
To: Alan Stern <stern@...land.harvard.edu>
Cc: Andrea Parri <parri.andrea@...il.com>, will@...nel.org,
	peterz@...radead.org, boqun.feng@...il.com, npiggin@...il.com,
	dhowells@...hat.com, j.alglave@....ac.uk, luc.maranget@...ia.fr,
	akiyks@...il.com, dlustig@...dia.com, joel@...lfernandes.org,
	linux-kernel@...r.kernel.org, hernan.poncedeleon@...weicloud.com,
	jonas.oberhauser@...weicloud.com
Subject: Re: New locking test for the paulmckrcu/litmus github archive

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@...land.harvard.edu>
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@...il.com>
    Signed-off-by: Alan Stern <stern@...land.harvard.edu>
    Signed-off-by: Paul E. McKenney <paulmck@...nel.org>

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)