linux-kernel - Re: Litmus test names

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives
Hash Suite: Windows password security audit tool. GUI, reports in PDF.
[<prev] [next>] [<thread-prev] [day] [month] [year] [list]
Message-ID: <20230409042916.GA768965@google.com>
Date:   Sun, 9 Apr 2023 04:29:16 +0000
From:   Joel Fernandes <joel@...lfernandes.org>
To:     Jonas Oberhauser <jonas.oberhauser@...weicloud.com>
Cc:     "Paul E. McKenney" <paulmck@...nel.org>,
        Alan Stern <stern@...land.harvard.edu>,
        linux-kernel@...r.kernel.org, Boqun Feng <boqun.feng@...il.com>,
        Jade Alglave <j.alglave@....ac.uk>,
        Luc Maranget <luc.maranget@...ia.fr>,
        Peter Zijlstra <peterz@...radead.org>,
        Will Deacon <will.deacon@....com>,
        Akira Yokosawa <akiyks@...il.com>,
        Andrea Parri <parri.andrea@...il.com>,
        Daniel Lustig <dlustig@...dia.com>,
        David Howells <dhowells@...hat.com>,
        Jonas Oberhauser <jonas.oberhauser@...wei.com>,
        linux-arch@...r.kernel.org, Nicholas Piggin <npiggin@...il.com>,
        Paul Heidekrüger <paul.heidekrueger@...tum.de>,
        Will Deacon <will@...nel.org>
Subject: Re: Litmus test names

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@...nel.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
> > 
>