Test ba

PPC ba (PPCBasicTen)
{
 P0:r1=y; P0:r2=1;
 P0:r5=x; P1:r5=x;
          P1:r6=y;
 x = z; y = 0; z=0 ; (* z is address 0, for nicer output in litmus *)
}

    P0       |      P1       ;
             |               ;
std r1,0,r5  | lwz r3,0,r6   ;
ld  r6,0,r5  | sync          ;
stw r2,0,r6  | ld  r4,0,r5   ;

(* Interesting, Adir et al claims this is allowed, but 
   my reading is that to be allowed, it requires "non-cumulative"
   barriers *)
(* Hard example, the local dependency on stores in P0
   must not be seen by P1, justify the patch of alien stores,
   and finally the introduction of store buffers *)
exists (P1:r3 = 1 /\ P1:r4=z);