Test dd4

PPC dd4 (DDFour)
"Double test, load;dep;store || load;dep;store"
{
 0:r2=2; 0:r4=x;
 1:r2=2; 1:r5=y;
 2:r1=1; 2:r4=x; 2:r5=y;
 3:r1=1; 3:r4=x; 3:r5=y;
}

P0          | P1         | P2           |P3          ;
stw r2,0(r4)|stw r2,0(r5)|lwz r2,0,r5   |lwz r2,0,r4 ;
            |            |xor r10,r2,r2 |xor r10,r2,r2;
            |            |stwx r1,r10,r4|stwx r1,r10,r5 ;

locations [x;y;]
exists (2:r2=1 /\ 3:r2=1)
(* Condition should be inverted: given state is a violation
   of causality! *)
(* The existence of  (2:r2=2 /\ 3:r2=2 /\x=2 /\y=2) is more intersting
*)