Litmus test names

Litmus test names

[Alan Stern]

Paul:

I just saw that two of the files in tools/memory-model/litmus-tests have 
almost identical names:

	Z6.0+pooncelock+pooncelock+pombonce.litmus
	Z6.0+pooncelock+poonceLock+pombonce.litmus

They differ only by a lower-case 'l' vs. a capital 'L'.  It's not at all 
easy to see, and won't play well in case-insensitive filesystems.

Should one of them be renamed?

Alan

Re: Litmus test names

[Paul E. McKenney]

On Thu, Apr 06, 2023 at 05:36:13PM -0400, Alan Stern wrote:
> Paul:
> 
> I just saw that two of the files in tools/memory-model/litmus-tests have 
> almost identical names:
> 
> 	Z6.0+pooncelock+pooncelock+pombonce.litmus
> 	Z6.0+pooncelock+poonceLock+pombonce.litmus
> 
> They differ only by a lower-case 'l' vs. a capital 'L'.  It's not at all 
> easy to see, and won't play well in case-insensitive filesystems.
> 
> Should one of them be renamed?

Quite possibly!

The "L" denotes smp_mb__after_spinlock().  The only code difference
between these is that Z6.0+pooncelock+poonceLock+pombonce.litmus has
smp_mb__after_spinlock() and Z6.0+pooncelock+pooncelock+pombonce.litmus
does not.

Suggestions for a better name?  We could capitalize all the letters
in LOCK, I suppose...

							Thanx, Paul

Re: Litmus test names

[Jonas Oberhauser]

On 4/7/2023 2:12 AM, Joel Fernandes wrote:
>
>
>> On Apr 6, 2023, at 6:34 PM, Paul E. McKenney <paulmck@kernel.org> wrote:
>>
>> On Thu, Apr 06, 2023 at 05:36:13PM -0400, Alan Stern wrote:
>>> Paul:
>>>
>>> I just saw that two of the files in tools/memory-model/litmus-tests 
>>> have
>>> almost identical names:
>>>
>>>  Z6.0+pooncelock+pooncelock+pombonce.litmus
>>>  Z6.0+pooncelock+poonceLock+pombonce.litmus
>>>
>>> They differ only by a lower-case 'l' vs. a capital 'L'.  It's not at 
>>> all
>>> easy to see, and won't play well in case-insensitive filesystems.
>>>
>>> Should one of them be renamed?
>>
>> Quite possibly!
>>
>> The "L" denotes smp_mb__after_spinlock().  The only code difference
>> between these is that Z6.0+pooncelock+poonceLock+pombonce.litmus has
>> smp_mb__after_spinlock() and Z6.0+pooncelock+pooncelock+pombonce.litmus
>> does not.
>>
>> Suggestions for a better name?  We could capitalize all the letters
>> in LOCK, I suppose...

I don't think capitalizing LOCK is helpful.

To be honest, almost all the names are extremely cryptic to newcomers 
like me (like, what does Z6.0 mean? Is it some magic incantation?).
And that's not something that's easy to fix.

The only use case I can think of for spending time improving the names 
is that sometimes you wanna say something like "oh, this is like 
Z6.0+pooncelock+pooncelockmb+pombonce". And then people can look up what 
that is.
For that, it's important that the names are easy to disambiguate by 
humans, and I think Joel's suggestion is an improvement.
(and it also fixes the issue brought up by Alan about case-insensitive 
file systems)

>
> Z6.0+pooncelock+pooncelockmb+pombonce.litmus ?
>
> Thanks,
>
>  - Joel
>


have fun, jonas

Re: Litmus test names

[Paul E. McKenney]

On Fri, Apr 07, 2023 at 03:05:01PM +0200, Jonas Oberhauser wrote:
> 
> 
> On 4/7/2023 2:12 AM, Joel Fernandes wrote:
> > 
> > 
> > > On Apr 6, 2023, at 6:34 PM, Paul E. McKenney <paulmck@kernel.org> wrote:
> > > 
> > > On Thu, Apr 06, 2023 at 05:36:13PM -0400, Alan Stern wrote:
> > > > Paul:
> > > > 
> > > > I just saw that two of the files in
> > > > tools/memory-model/litmus-tests have
> > > > almost identical names:
> > > > 
> > > >  Z6.0+pooncelock+pooncelock+pombonce.litmus
> > > >  Z6.0+pooncelock+poonceLock+pombonce.litmus
> > > > 
> > > > They differ only by a lower-case 'l' vs. a capital 'L'.  It's
> > > > not at all
> > > > easy to see, and won't play well in case-insensitive filesystems.
> > > > 
> > > > Should one of them be renamed?
> > > 
> > > Quite possibly!
> > > 
> > > The "L" denotes smp_mb__after_spinlock().  The only code difference
> > > between these is that Z6.0+pooncelock+poonceLock+pombonce.litmus has
> > > smp_mb__after_spinlock() and Z6.0+pooncelock+pooncelock+pombonce.litmus
> > > does not.
> > > 
> > > Suggestions for a better name?  We could capitalize all the letters
> > > in LOCK, I suppose...
> 
> I don't think capitalizing LOCK is helpful.

Greek font, then?  (Sorry, couldn't resist...)

> To be honest, almost all the names are extremely cryptic to newcomers like
> me (like, what does Z6.0 mean? Is it some magic incantation?).
> And that's not something that's easy to fix.

All too true on all counts.  Some of the names abbreviate the litmus
test itself, and there are multiple encodings depending one who/what
generated the test in question.  Others of the names relate to who came
up with them or the code from which they are derived.

New allegedly universal naming schemes have a rather short half-life.

What would be cool would be a way to structurally compare litmus tests.
I bet that there are quite a few duplicates, for example.

> The only use case I can think of for spending time improving the names is
> that sometimes you wanna say something like "oh, this is like
> Z6.0+pooncelock+pooncelockmb+pombonce". And then people can look up what
> that is.
> For that, it's important that the names are easy to disambiguate by humans,
> and I think Joel's suggestion is an improvement.
> (and it also fixes the issue brought up by Alan about case-insensitive file
> systems)
> 
> > 
> > Z6.0+pooncelock+pooncelockmb+pombonce.litmus ?

I am OK with this one, but then again, I was also OK with the original
Z6.0+pooncelock+poonceLock+pombonce.litmus.  ;-)

Would someone like to to a "git mv" send the resulting patch?

							Thanx, Paul

Re: Litmus test names

[Joel Fernandes]

On Fri, Apr 07, 2023 at 05:49:02PM -0700, Paul E. McKenney wrote:
> On Fri, Apr 07, 2023 at 03:05:01PM +0200, Jonas Oberhauser wrote:
> > 
> > 
> > On 4/7/2023 2:12 AM, Joel Fernandes wrote:
> > > 
> > > 
> > > > On Apr 6, 2023, at 6:34 PM, Paul E. McKenney <paulmck@kernel.org> wrote:
> > > > 
> > > > On Thu, Apr 06, 2023 at 05:36:13PM -0400, Alan Stern wrote:
> > > > > Paul:
> > > > > 
> > > > > I just saw that two of the files in
> > > > > tools/memory-model/litmus-tests have
> > > > > almost identical names:
> > > > > 
> > > > >  Z6.0+pooncelock+pooncelock+pombonce.litmus
> > > > >  Z6.0+pooncelock+poonceLock+pombonce.litmus
> > > > > 
> > > > > They differ only by a lower-case 'l' vs. a capital 'L'.  It's
> > > > > not at all
> > > > > easy to see, and won't play well in case-insensitive filesystems.
> > > > > 
> > > > > Should one of them be renamed?
> > > > 
> > > > Quite possibly!
> > > > 
> > > > The "L" denotes smp_mb__after_spinlock().  The only code difference
> > > > between these is that Z6.0+pooncelock+poonceLock+pombonce.litmus has
> > > > smp_mb__after_spinlock() and Z6.0+pooncelock+pooncelock+pombonce.litmus
> > > > does not.
> > > > 
> > > > Suggestions for a better name?  We could capitalize all the letters
> > > > in LOCK, I suppose...
> > 
> > I don't think capitalizing LOCK is helpful.
> 
> Greek font, then?  (Sorry, couldn't resist...)
> 
> > To be honest, almost all the names are extremely cryptic to newcomers like
> > me (like, what does Z6.0 mean? Is it some magic incantation?).
> > And that's not something that's easy to fix.
> 
> All too true on all counts.  Some of the names abbreviate the litmus
> test itself, and there are multiple encodings depending one who/what
> generated the test in question.  Others of the names relate to who came
> up with them or the code from which they are derived.
> 
> New allegedly universal naming schemes have a rather short half-life.
> 
> What would be cool would be a way to structurally compare litmus tests.
> I bet that there are quite a few duplicates, for example.
> 
> > The only use case I can think of for spending time improving the names is
> > that sometimes you wanna say something like "oh, this is like
> > Z6.0+pooncelock+pooncelockmb+pombonce". And then people can look up what
> > that is.
> > For that, it's important that the names are easy to disambiguate by humans,
> > and I think Joel's suggestion is an improvement.
> > (and it also fixes the issue brought up by Alan about case-insensitive file
> > systems)
> > 
> > > 
> > > Z6.0+pooncelock+pooncelockmb+pombonce.litmus ?
> 
> I am OK with this one, but then again, I was also OK with the original
> Z6.0+pooncelock+poonceLock+pombonce.litmus.  ;-)

FWIW, if I move that smp_mb_after..() a step lower, that also makes the test
work (see below).

If you may look over quickly my analysis of why this smp_mb_after..() is
needed, it is because what I marked as a and d below don't have an hb
relation right?

(*
  b ->rf c

  d ->co e

  e ->hb f

  basically the issue is a ->po b ->rf c ->po d    does not imply a ->hb d
*)

P0(int *x, int *y, spinlock_t *mylock)
{
	spin_lock(mylock);
	WRITE_ONCE(*x, 1); // a
	WRITE_ONCE(*y, 1); // b
	spin_unlock(mylock);
}

P1(int *y, int *z, spinlock_t *mylock)
{
	int r0;

	spin_lock(mylock);
	r0 = READ_ONCE(*y); // c
	smp_mb__after_spinlock(); // moving this a bit lower also works fwiw.
	WRITE_ONCE(*z, 1);  // d
	spin_unlock(mylock);
}

P2(int *x, int *z)
{
	int r1;

	WRITE_ONCE(*z, 2);  // e
	smp_mb();
	r1 = READ_ONCE(*x); // f
}

exists (1:r0=1 /\ z=2 /\ 2:r1=0)


> Would someone like to to a "git mv" send the resulting patch?

Yes I can do that in return as I am thankful in advance for the above
discussion. ;)

thanks,

 - Joel

Re: Litmus test names

[Jonas Oberhauser]

On 4/8/2023 6:49 PM, Joel Fernandes wrote:
> On Fri, Apr 07, 2023 at 05:49:02PM -0700, Paul E. McKenney wrote:
>> On Fri, Apr 07, 2023 at 03:05:01PM +0200, Jonas Oberhauser wrote:
>>>
>>> On 4/7/2023 2:12 AM, Joel Fernandes wrote:
>>>>
>>>>> On Apr 6, 2023, at 6:34 PM, Paul E. McKenney <paulmck@kernel.org> wrote:
>>>>>
>>>>> On Thu, Apr 06, 2023 at 05:36:13PM -0400, Alan Stern wrote:
>>>>>> Paul:
>>>>>>
>>>>>> I just saw that two of the files in
>>>>>> tools/memory-model/litmus-tests have
>>>>>> almost identical names:
>>>>>>
>>>>>>   Z6.0+pooncelock+pooncelock+pombonce.litmus
>>>>>>   Z6.0+pooncelock+poonceLock+pombonce.litmus
>>>>>>
>>>>>> They differ only by a lower-case 'l' vs. a capital 'L'.  It's
>>>>>> not at all
>>>>>> easy to see, and won't play well in case-insensitive filesystems.
>>>>>>
>>>>>> Should one of them be renamed?
>>>>>
> FWIW, if I move that smp_mb_after..() a step lower, that also makes the test
> work (see below).
>
> If you may look over quickly my analysis of why this smp_mb_after..() is
> needed, it is because what I marked as a and d below don't have an hb
> relation right?

I think a and d have an hb relation due to the
a ->po-rel X ->rfe Y ->acq-po d
edges (where X and Y are the unlock/lock events I annotated in your 
example below).

Generally, an mb_unlock_lock isn't used to give you hb, but to turn some 
(coe/fre) ; hb* edges into pb edges

In this case, that would probably be
f ->fre a ->hb* f   (where a ->hb* f comes from a ->hb* d ->hb e ->hb f)
By adding the mb_unlock_lock_po in one of the right places, this becomes 
f ->pb f,
thus forbidden.


Have fun,
jonas


>
> (*
>    b ->rf c
>
>    d ->co e
>
>    e ->hb f
>
>    basically the issue is a ->po b ->rf c ->po d    does not imply a ->hb d
> *)
>
> P0(int *x, int *y, spinlock_t *mylock)
> {
> 	spin_lock(mylock);
> 	WRITE_ONCE(*x, 1); // a
> 	WRITE_ONCE(*y, 1); // b
> 	spin_unlock(mylock); // X
> }
>
> P1(int *y, int *z, spinlock_t *mylock)
> {
> 	int r0;
>
> 	spin_lock(mylock); // Y
> 	r0 = READ_ONCE(*y); // c
> 	smp_mb__after_spinlock(); // moving this a bit lower also works fwiw.
> 	WRITE_ONCE(*z, 1);  // d
> 	spin_unlock(mylock);
> }
>
> P2(int *x, int *z)
> {
> 	int r1;
>
> 	WRITE_ONCE(*z, 2);  // e
> 	smp_mb();
> 	r1 = READ_ONCE(*x); // f
> }
>
> exists (1:r0=1 /\ z=2 /\ 2:r1=0)
>
>
>> Would someone like to to a "git mv" send the resulting patch?
> Yes I can do that in return as I am thankful in advance for the above
> discussion. ;)
>
> thanks,
>
>   - Joel
>

Re: Litmus test names

[Paul E. McKenney]

On Sat, Apr 08, 2023 at 08:57:57PM +0200, Jonas Oberhauser wrote:
> 
> On 4/8/2023 6:49 PM, Joel Fernandes wrote:
> > On Fri, Apr 07, 2023 at 05:49:02PM -0700, Paul E. McKenney wrote:
> > > On Fri, Apr 07, 2023 at 03:05:01PM +0200, Jonas Oberhauser wrote:
> > > > 
> > > > On 4/7/2023 2:12 AM, Joel Fernandes wrote:
> > > > > 
> > > > > > On Apr 6, 2023, at 6:34 PM, Paul E. McKenney <paulmck@kernel.org> wrote:
> > > > > > 
> > > > > > On Thu, Apr 06, 2023 at 05:36:13PM -0400, Alan Stern wrote:
> > > > > > > Paul:
> > > > > > > 
> > > > > > > I just saw that two of the files in
> > > > > > > tools/memory-model/litmus-tests have
> > > > > > > almost identical names:
> > > > > > > 
> > > > > > >   Z6.0+pooncelock+pooncelock+pombonce.litmus
> > > > > > >   Z6.0+pooncelock+poonceLock+pombonce.litmus
> > > > > > > 
> > > > > > > They differ only by a lower-case 'l' vs. a capital 'L'.  It's
> > > > > > > not at all
> > > > > > > easy to see, and won't play well in case-insensitive filesystems.
> > > > > > > 
> > > > > > > Should one of them be renamed?
> > > > > > 
> > FWIW, if I move that smp_mb_after..() a step lower, that also makes the test
> > work (see below).
> > 
> > If you may look over quickly my analysis of why this smp_mb_after..() is
> > needed, it is because what I marked as a and d below don't have an hb
> > relation right?
> 
> I think a and d have an hb relation due to the
> a ->po-rel X ->rfe Y ->acq-po d
> edges (where X and Y are the unlock/lock events I annotated in your example
> below).
> 
> Generally, an mb_unlock_lock isn't used to give you hb, but to turn some
> (coe/fre) ; hb* edges into pb edges
> 
> In this case, that would probably be
> f ->fre a ->hb* f   (where a ->hb* f comes from a ->hb* d ->hb e ->hb f)
> By adding the mb_unlock_lock_po in one of the right places, this becomes f
> ->pb f,
> thus forbidden.

Yes, it is forbidden, and even on purpose.  ;-)

But please don't do this in real life.  Having that READ_ONCE(*y) be
ordered differently on different architectures is not what those reading
your code will want to deal with.

							Thanx, Paul

> Have fun,
> jonas
> 
> 
> > 
> > (*
> >    b ->rf c
> > 
> >    d ->co e
> > 
> >    e ->hb f
> > 
> >    basically the issue is a ->po b ->rf c ->po d    does not imply a ->hb d
> > *)
> > 
> > P0(int *x, int *y, spinlock_t *mylock)
> > {
> > 	spin_lock(mylock);
> > 	WRITE_ONCE(*x, 1); // a
> > 	WRITE_ONCE(*y, 1); // b
> > 	spin_unlock(mylock); // X
> > }
> > 
> > P1(int *y, int *z, spinlock_t *mylock)
> > {
> > 	int r0;
> > 
> > 	spin_lock(mylock); // Y
> > 	r0 = READ_ONCE(*y); // c
> > 	smp_mb__after_spinlock(); // moving this a bit lower also works fwiw.
> > 	WRITE_ONCE(*z, 1);  // d
> > 	spin_unlock(mylock);
> > }
> > 
> > P2(int *x, int *z)
> > {
> > 	int r1;
> > 
> > 	WRITE_ONCE(*z, 2);  // e
> > 	smp_mb();
> > 	r1 = READ_ONCE(*x); // f
> > }
> > 
> > exists (1:r0=1 /\ z=2 /\ 2:r1=0)
> > 
> > 
> > > Would someone like to to a "git mv" send the resulting patch?
> > Yes I can do that in return as I am thankful in advance for the above
> > discussion. ;)
> > 
> > thanks,
> > 
> >   - Joel
> > 
> 

Re: Litmus test names

[Joel Fernandes]

On Sat, Apr 08, 2023 at 08:57:57PM +0200, Jonas Oberhauser wrote:
> 
> On 4/8/2023 6:49 PM, Joel Fernandes wrote:
> > On Fri, Apr 07, 2023 at 05:49:02PM -0700, Paul E. McKenney wrote:
> > > On Fri, Apr 07, 2023 at 03:05:01PM +0200, Jonas Oberhauser wrote:
> > > > 
> > > > On 4/7/2023 2:12 AM, Joel Fernandes wrote:
> > > > > 
> > > > > > On Apr 6, 2023, at 6:34 PM, Paul E. McKenney <paulmck@kernel.org> wrote:
> > > > > > 
> > > > > > On Thu, Apr 06, 2023 at 05:36:13PM -0400, Alan Stern wrote:
> > > > > > > Paul:
> > > > > > > 
> > > > > > > I just saw that two of the files in
> > > > > > > tools/memory-model/litmus-tests have
> > > > > > > almost identical names:
> > > > > > > 
> > > > > > >   Z6.0+pooncelock+pooncelock+pombonce.litmus
> > > > > > >   Z6.0+pooncelock+poonceLock+pombonce.litmus
> > > > > > > 
> > > > > > > They differ only by a lower-case 'l' vs. a capital 'L'.  It's
> > > > > > > not at all
> > > > > > > easy to see, and won't play well in case-insensitive filesystems.
> > > > > > > 
> > > > > > > Should one of them be renamed?
> > > > > > 
> > FWIW, if I move that smp_mb_after..() a step lower, that also makes the test
> > work (see below).
> > 
> > If you may look over quickly my analysis of why this smp_mb_after..() is
> > needed, it is because what I marked as a and d below don't have an hb
> > relation right?
> 
> I think a and d have an hb relation due to the
> a ->po-rel X ->rfe Y ->acq-po d
> edges (where X and Y are the unlock/lock events I annotated in your example
> below).

I kind of disagree with that, because if I understand correctly, a ->hb d
means ALL CPUs agree as a universal fact that a happened before d.

Clearly, without the smp_mb(), CPU P2 disagrees that a happened before d.

So the po-rel acq-po doesn't imply a->hb d, IMHO. Correct me if I'm wrong
though with any counter example. ;-)

> 
> Generally, an mb_unlock_lock isn't used to give you hb, but to turn some
> (coe/fre) ; hb* edges into pb edges
> 
> In this case, that would probably be
> f ->fre a ->hb* f   (where a ->hb* f comes from a ->hb* d ->hb e ->hb f)
> By adding the mb_unlock_lock_po in one of the right places, this becomes f
> ->pb f,
> thus forbidden.

This I fully agree with. I observed this litmus is actually the R-pattern
with P0 split into 2 CPUs by spltting the thread of execution using a lock
and ordering them with an ->rfe and the exists() clause.

Otherwise it is identical.

In the R-pattern also, you need an smp_mb() between the pair of accesses.

Using the same annotations but instead applying them to the R-pattern, it
looks like:

 P0(int *x, int *y)
 {
 	WRITE_ONCE(*x, 1); // a
	// Here we need an smp_mb() to order the stores to x and z.
 	WRITE_ONCE(*z, 1);  // d
 }

 P2(int *x, int *z)
 {
 	int r1;
 
 	WRITE_ONCE(*z, 2);  // e
 	smp_mb();
 	r1 = READ_ONCE(*x); // f

exists (z=2 /\ 2:r1=0)


thanks,

 - Joel


> 
> Have fun,
> jonas
> 
> 
> > 
> > (*
> >    b ->rf c
> > 
> >    d ->co e
> > 
> >    e ->hb f
> > 
> >    basically the issue is a ->po b ->rf c ->po d    does not imply a ->hb d
> > *)
> > 
> > P0(int *x, int *y, spinlock_t *mylock)
> > {
> > 	spin_lock(mylock);
> > 	WRITE_ONCE(*x, 1); // a
> > 	WRITE_ONCE(*y, 1); // b
> > 	spin_unlock(mylock); // X
> > }
> > 
> > P1(int *y, int *z, spinlock_t *mylock)
> > {
> > 	int r0;
> > 
> > 	spin_lock(mylock); // Y
> > 	r0 = READ_ONCE(*y); // c
> > 	smp_mb__after_spinlock(); // moving this a bit lower also works fwiw.
> > 	WRITE_ONCE(*z, 1);  // d
> > 	spin_unlock(mylock);
> > }
> > 
> > P2(int *x, int *z)
> > {
> > 	int r1;
> > 
> > 	WRITE_ONCE(*z, 2);  // e
> > 	smp_mb();
> > 	r1 = READ_ONCE(*x); // f
> > }
> > 
> > exists (1:r0=1 /\ z=2 /\ 2:r1=0)
> > 
> > 
> > > Would someone like to to a "git mv" send the resulting patch?
> > Yes I can do that in return as I am thankful in advance for the above
> > discussion. ;)
> > 
> > thanks,
> > 
> >   - Joel
> > 
> 

RE: Litmus test names

[David Laight]

From: Alan Stern
> Sent: 06 April 2023 22:36
> 
> Paul:
> 
> I just saw that two of the files in tools/memory-model/litmus-tests have
> almost identical names:
> 
> 	Z6.0+pooncelock+pooncelock+pombonce.litmus
> 	Z6.0+pooncelock+poonceLock+pombonce.litmus
> 
> They differ only by a lower-case 'l' vs. a capital 'L'.  It's not at all
> easy to see, and won't play well in case-insensitive filesystems.

Change the 'L' to a '1' - that'll be ok on case-insensitive
filesystems :-)

	David

-
Registered Address Lakeside, Bramley Road, Mount Farm, Milton Keynes, MK1 1PT, UK
Registration No: 1397386 (Wales)

Re: Litmus test names

[Paul E. McKenney]

On Mon, Apr 10, 2023 at 10:43:52AM +0000, David Laight wrote:
> From: Alan Stern
> > Sent: 06 April 2023 22:36
> > 
> > Paul:
> > 
> > I just saw that two of the files in tools/memory-model/litmus-tests have
> > almost identical names:
> > 
> > 	Z6.0+pooncelock+pooncelock+pombonce.litmus
> > 	Z6.0+pooncelock+poonceLock+pombonce.litmus
> > 
> > They differ only by a lower-case 'l' vs. a capital 'L'.  It's not at all
> > easy to see, and won't play well in case-insensitive filesystems.
> 
> Change the 'L' to a '1' - that'll be ok on case-insensitive
> filesystems :-)

Or just name them all using SHA-1 of the file contents?  ;-)

							Thanx, Paul