Test wrcv4

PPC wrcv4 (PPCWRCFour)
"write-to_read causality, boehm adve PLDI'08 (Fig 5.)"
{
P0:r1=x;
P1:r1=x; P1:r2=y;
P2:r1=x; P2:r3=z;
P3:r2=y ;P3:r3=z;
P0:r9=1; P1:r9=1; P3:r9=1;
} 
      P0    |       P1   |   P2           | P3         ;
stw r9,0,r1 |lwz r5,0,r1 |lwz r5,0,r3     |lwz r5,0,r2 ;
            |            |xor r10,r5,r5   |            ;
            |stw r9,0,r2 |lwzx r6,r10,r1  |stw  r9,0,r3;

exists (P1:r5=1 /\ P2:r5=1 /\ P3:r5=1 /\ P2:r6=0)
(* Variations on ppc-cpp.wrc-adir2.litmus*)