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

Paul E. McKenney
2016-09-29T20:26:48Z

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