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

[Paul E. McKenney]

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 <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.
> > > 
> > > 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 <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 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);
}