Received-SPF: pass (google.com: domain of linux-kernel+bounces-203054-linux.lists.archive=gmail.com@vger.kernel.org designates 147.75.199.223 as permitted sender) client-ip=147.75.199.223;
Date: Wed, 5 Jun 2024 11:25:11 -0700
From: "Paul E. McKenney" <paulmck@kernel.org>
To: Alan Stern <stern@rowland.harvard.edu>
Cc: Andrea Parri <parri.andrea@gmail.com>, will@kernel.org,
	peterz@infradead.org, boqun.feng@gmail.com, npiggin@gmail.com,
	dhowells@redhat.com, j.alglave@ucl.ac.uk, luc.maranget@inria.fr,
	akiyks@gmail.com, dlustig@nvidia.com, joel@joelfernandes.org,
	linux-kernel@vger.kernel.org, hernan.poncedeleon@huaweicloud.com,
	jonas.oberhauser@huaweicloud.com
Subject: Re: New locking test for the paulmckrcu/litmus github archive
Message-ID: <df851df5-0e3a-45b1-ae85-9625309766b0@paulmck-laptop>
Reply-To: paulmck@kernel.org
References: <a8c06694-098d-4b95-845c-96b40cd3ff2d@rowland.harvard.edu>
Precedence: bulk
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <a8c06694-098d-4b95-845c-96b40cd3ff2d@rowland.harvard.edu>

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@rowland.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@gmail.com>
    Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
    Signed-off-by: Paul E. McKenney <paulmck@kernel.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)