Test wrcv5

PPC wrcv5 (PPCWRCFive)
"write-to_read causality, boehm adve PLDI'08 (Fig 5.)"
(Paul Mc Keene 'solution')
{
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  ;
            | lwsync      | cmpw r5,r5   ;
            | stw r9,0,r2 | bne L2       ;
            |             | isync        ;
            |             | lwz r6,0,r1  ;
            |             | L2:          ;
exists (1:r5=1 /\ 2:r5=1 /\ 2:r6=0)