Messages in this thread | | | Date | Thu, 29 Sep 2016 13:26:41 -0700 | From | "Paul E. McKenney" <> | Subject | Re: [PATCH locking/Documentation 1/2] Add note of release-acquire store vulnerability |
| |
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
| |