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

[Alan Stern]

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.

Alan