[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]
Message-ID: <df851df5-0e3a-45b1-ae85-9625309766b0@paulmck-laptop>
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)
Powered by blists - more mailing lists