Re: Litmus test names

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

 




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@xxxxxxxxxx> 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





[Index of Archives]     [Linux Kernel]     [Kernel Newbies]     [x86 Platform Driver]     [Netdev]     [Linux Wireless]     [Netfilter]     [Bugtraq]     [Linux Filesystems]     [Yosemite Discussion]     [MIPS Linux]     [ARM Linux]     [Linux Security]     [Linux RAID]     [Samba]     [Device Mapper]

  Powered by Linux