2024-06-05 14:47:18

by Alan Stern

[permalink] [raw]
Subject: New locking test for the paulmckrcu/litmus github archive

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)


2024-06-05 18:25:19

by Paul E. McKenney

[permalink] [raw]
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 <[email protected]>
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 <[email protected]>
Signed-off-by: Alan Stern <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>

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)

2024-06-05 18:40:15

by Alan Stern

[permalink] [raw]
Subject: Re: New locking test for the paulmckrcu/litmus github archive

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 <[email protected]>
> 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)

2024-06-06 17:14:45

by Paul E. McKenney

[permalink] [raw]
Subject: Re: New locking test for the paulmckrcu/litmus github archive

On Wed, Jun 05, 2024 at 02:40:05PM -0400, Alan Stern wrote:
> 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 <[email protected]>
> > 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:

Good point, the deadlock is irrelevant. If I want to make that point,
I can add a test that really does deadlock. ;-)

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

I ended up with the following:

This has no executions. After the fix, there is one execution
that matches the "exists" clause and no executions that do not
match, hence an "Always" result.

The reason for explicitly stating "This has no executions" is that a
lot of people never have seen such a thing.

> > 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?)

The CoWWW comes from me having been confused. The new filename is
CoWW+sil-lock-sil-unlock-sil.litmus. Thank you for spotting this!

> > +
> > +(*
> > + * 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?

Done! Please see below for the updated commit.

Thanx, Paul

------------------------------------------------------------------------

commit d4d216a08b4bedb8cdb0f57a224a4e331b35b931
Author: Alan Stern <[email protected]>
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 CoWW+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 has no executions. After the fix, there is one execution that
matches the "exists" clause and no executions that do not match, hence an
"Always" result.

Suggested-by: Andrea Parri <[email protected]>
Signed-off-by: Alan Stern <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>

diff --git a/manual/locked/CoWW+sil-lock-sil-unlock-sil.litmus b/manual/locked/CoWW+sil-lock-sil-unlock-sil.litmus
new file mode 100644
index 00000000..aadc4ceb
--- /dev/null
+++ b/manual/locked/CoWW+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)

2024-06-06 17:25:23

by Alan Stern

[permalink] [raw]
Subject: Re: New locking test for the paulmckrcu/litmus github archive

On Thu, Jun 06, 2024 at 10:07:35AM -0700, Paul E. McKenney wrote:
> On Wed, Jun 05, 2024 at 02:40:05PM -0400, Alan Stern wrote:
> > 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 <[email protected]>
> > > 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:
>
> Good point, the deadlock is irrelevant. If I want to make that point,
> I can add a test that really does deadlock. ;-)
>
> > After the fix, there should be one execution that matches the
> > "exists" clause and no executions that don't match, hence an
> > "Always" result.
>
> I ended up with the following:
>
> This has no executions. After the fix, there is one execution
> that matches the "exists" clause and no executions that do not
> match, hence an "Always" result.
>
> The reason for explicitly stating "This has no executions" is that a
> lot of people never have seen such a thing.

Okay. Don't we already have a litmus test in the archive that really
does create a deadlock? Something like: Lock Lock Unlock Unlock, all
using the same lock variable?

> > > 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?)
>
> The CoWWW comes from me having been confused. The new filename is
> CoWW+sil-lock-sil-unlock-sil.litmus. Thank you for spotting this!

All right, but what does the "CoWW" part stand for?

> > > +
> > > +(*
> > > + * 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?
>
> Done! Please see below for the updated commit.
>
> Thanx, Paul
>
> ------------------------------------------------------------------------
>
> commit d4d216a08b4bedb8cdb0f57a224a4e331b35b931
> Author: Alan Stern <[email protected]>
> 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 CoWW+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

Maybe you better re-run this with the updated litmus test file. Those
two lines aren't right.

Alan

2024-06-06 17:58:59

by Paul E. McKenney

[permalink] [raw]
Subject: Re: New locking test for the paulmckrcu/litmus github archive

On Thu, Jun 06, 2024 at 01:21:28PM -0400, Alan Stern wrote:
> On Thu, Jun 06, 2024 at 10:07:35AM -0700, Paul E. McKenney wrote:
> > On Wed, Jun 05, 2024 at 02:40:05PM -0400, Alan Stern wrote:
> > > 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 <[email protected]>
> > > > 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:
> >
> > Good point, the deadlock is irrelevant. If I want to make that point,
> > I can add a test that really does deadlock. ;-)
> >
> > > After the fix, there should be one execution that matches the
> > > "exists" clause and no executions that don't match, hence an
> > > "Always" result.
> >
> > I ended up with the following:
> >
> > This has no executions. After the fix, there is one execution
> > that matches the "exists" clause and no executions that do not
> > match, hence an "Always" result.
> >
> > The reason for explicitly stating "This has no executions" is that a
> > lot of people never have seen such a thing.
>
> Okay. Don't we already have a litmus test in the archive that really
> does create a deadlock? Something like: Lock Lock Unlock Unlock, all
> using the same lock variable?

We do have these guys:

auto/C-RR-GR+RR-R+RR-R.litmus
auto/C-RR-GR+RR-R.litmus
auto/C-RW-GR+RW-R+RW-R.litmus
auto/C-RW-GR+RW-R.litmus
auto/C-WR-GR+WR-R+WR-R.litmus
auto/C-WR-GR+WR-R.litmus
auto/C-WW-GR+WW-R+WW-R.litmus
auto/C-WW-GR+WW-R.litmus
A synchronize_rcu() in an RCU read-side critical section.

I added a manual/locked/self-deadlock.litmus, which is shown at the
end of this email. Omitting the nested self-deadlocking acquisition
and release gives one state with blank line. ;-)

Or should I add a spin_is_locked() in order to get a non-empty
state line?

> > > > 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?)
> >
> > The CoWWW comes from me having been confused. The new filename is
> > CoWW+sil-lock-sil-unlock-sil.litmus. Thank you for spotting this!
>
> All right, but what does the "CoWW" part stand for?

"Coherence, Write-Write".

> > > > +
> > > > +(*
> > > > + * 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?
> >
> > Done! Please see below for the updated commit.
> >
> > Thanx, Paul
> >
> > ------------------------------------------------------------------------
> >
> > commit d4d216a08b4bedb8cdb0f57a224a4e331b35b931
> > Author: Alan Stern <[email protected]>
> > 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 CoWW+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
>
> Maybe you better re-run this with the updated litmus test file. Those
> two lines aren't right.

Hah! I forgot to update the name of the test within the file. Fixed
now, again, thank you.

Thanx, Paul

------------------------------------------------------------------------

C self-deadlock
(*
* Result: DEADLOCK
*
* Locking self-deadlock on process 0.
*)
{
}

P0(spinlock_t *sl)
{
spin_lock(sl);
spin_lock(sl);
spin_unlock(sl);
spin_unlock(sl);
}

2024-06-06 18:52:11

by Alan Stern

[permalink] [raw]
Subject: Re: New locking test for the paulmckrcu/litmus github archive

On Thu, Jun 06, 2024 at 10:57:42AM -0700, Paul E. McKenney wrote:
> On Thu, Jun 06, 2024 at 01:21:28PM -0400, Alan Stern wrote:
> > Okay. Don't we already have a litmus test in the archive that really
> > does create a deadlock? Something like: Lock Lock Unlock Unlock, all
> > using the same lock variable?
>
> We do have these guys:
>
> auto/C-RR-GR+RR-R+RR-R.litmus
> auto/C-RR-GR+RR-R.litmus
> auto/C-RW-GR+RW-R+RW-R.litmus
> auto/C-RW-GR+RW-R.litmus
> auto/C-WR-GR+WR-R+WR-R.litmus
> auto/C-WR-GR+WR-R.litmus
> auto/C-WW-GR+WW-R+WW-R.litmus
> auto/C-WW-GR+WW-R.litmus
> A synchronize_rcu() in an RCU read-side critical section.
>
> I added a manual/locked/self-deadlock.litmus, which is shown at the
> end of this email. Omitting the nested self-deadlocking acquisition
> and release gives one state with blank line. ;-)

Hah, because there is no "exists" clause and no variables other than the
spinlock itself.

> Or should I add a spin_is_locked() in order to get a non-empty
> state line?

It's fine the way it is.

Alan

2024-06-06 19:00:35

by Paul E. McKenney

[permalink] [raw]
Subject: Re: New locking test for the paulmckrcu/litmus github archive

On Thu, Jun 06, 2024 at 02:52:02PM -0400, Alan Stern wrote:
> On Thu, Jun 06, 2024 at 10:57:42AM -0700, Paul E. McKenney wrote:
> > On Thu, Jun 06, 2024 at 01:21:28PM -0400, Alan Stern wrote:
> > > Okay. Don't we already have a litmus test in the archive that really
> > > does create a deadlock? Something like: Lock Lock Unlock Unlock, all
> > > using the same lock variable?
> >
> > We do have these guys:
> >
> > auto/C-RR-GR+RR-R+RR-R.litmus
> > auto/C-RR-GR+RR-R.litmus
> > auto/C-RW-GR+RW-R+RW-R.litmus
> > auto/C-RW-GR+RW-R.litmus
> > auto/C-WR-GR+WR-R+WR-R.litmus
> > auto/C-WR-GR+WR-R.litmus
> > auto/C-WW-GR+WW-R+WW-R.litmus
> > auto/C-WW-GR+WW-R.litmus
> > A synchronize_rcu() in an RCU read-side critical section.
> >
> > I added a manual/locked/self-deadlock.litmus, which is shown at the
> > end of this email. Omitting the nested self-deadlocking acquisition
> > and release gives one state with blank line. ;-)
>
> Hah, because there is no "exists" clause and no variables other than the
> spinlock itself.

;-) ;-) ;-)

> > Or should I add a spin_is_locked() in order to get a non-empty
> > state line?
>
> It's fine the way it is.

Very good, pushed.

Thanx, Paul