Test wrcv3

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

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