Re: [PATCH locking/Documentation 1/2] Add note of release-acquire store vulnerability

[Paul E. McKenney]

On Thu, Sep 29, 2016 at 03:36:38PM -0400, Alan Stern wrote:
> On Thu, 29 Sep 2016, Paul E. McKenney wrote:
> 
> > On Thu, Sep 29, 2016 at 08:44:39PM +0200, Peter Zijlstra wrote:
> 
> > > How about something like so on PPC?
> > > 
> > > P0(int *x, int *y)
> > > {
> > > 	WRITE_ONCE(*x, 1);
> > > 	smp_store_release(y, 1);
> > > }
> > > 
> > > P1(int *x, int *y)
> > > {
> > > 	WRITE_ONCE(x, 2);
> > 
> > Need "WRITE_ONCE(*x, 2)" here.
> > 
> > > 	smp_store_release(y, 2);
> > > }
> > > 
> > > P2(int *x, int *y)
> > > {
> > > 	r1 = smp_load_acquire(y);
> > > 	r2 = READ_ONCE(*x);
> > > }
> > > 
> > > (((x==1 && y==2) | (x==2 && y==1)) && (r1==1 || r1==2) && r2==0)
> > 
> > That exists-clause is quite dazzling...  So if each of P0 and P1
> > win, but on different stores, and if P2 follows one or the other
> > of P0 or P1, can r2 get the pre-initialization value for x?
> 
> In fact, this is more than you need.  It's enough to specify
> 
> exists (2:r1=1 \/ 2:r1=2) /\ 2:r2=0
> 
> This much already is forbidden.  For the sake of argument, say r1=1.  
> Then P2 has read from P1's store-release.  By definition, P1's write to
> x is visible to P2, so r2 will get the value from that write or from
> one that is later in x's coherence order.  In other words, r2 will end
> up equal to either 1 or 2, but not 0.
> 
> > > If you execute P0 and P1 concurrently and one store of each 'wins' the
> > > LWSYNC of either is null and void, and therefore P2 is unordered and can
> > > observe r2==0.
> 
> Not so.  lwsync instructions cannot be "voided".
> 
> > That vaguely resembles the infamous Z6.3, but only vaguely.  The Linux-kernel
> > memory model says "forbidden" to this:
> > 
> > 	C C-WillDeacon-AcqRelStore.litmus
> > 
> > 	{
> > 	}
> > 
> > 	P0(int *x, int *y)
> > 	{
> > 	      WRITE_ONCE(*x, 1);
> > 	      smp_store_release(y, 1);
> > 	}
> > 
> > 	P1(int *x, int *y)
> > 	{
> > 	      WRITE_ONCE(*x, 2);
> > 	      smp_store_release(y, 2);
> > 	}
> > 
> > 	P2(int *x, int *y)
> > 	{
> > 	      r1 = smp_load_acquire(y);
> > 	      r2 = READ_ONCE(*x);
> > 	}
> > 
> > 	exists
> > 	(((x=1 /\ y=2) \/ (x=2 /\ y=1)) /\ (2:r1=1 \/ 2:r1=2) /\ 2:r2=0)
> 
> As above, you can leave out the part about the final values for x and 
> y.  The test will still be forbidden.
> 
> On the other hand, there's no guarantee that if r1=1 at the end then r2 
> will also be 1.  It's quite possible that r1=1 and r2=2, or vice versa.

And herd agrees for both the kernel model and the powerpc translation.
I killed PPCMEM, which was up to 1.2G of state space.  So is this a
case where "herd -cat ppc.cat" can be trusted?  ;-)

And the web ppcmem does not allow the exists clause, from what I could
see.

							Thanx, Paul