PPC dd3 (DDThree) "Double test, load;lwsync;store || load;lwsync;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 ; | |lwsync |lwsync ; | |stw r1,0,r4|stw r1,0,r5 ; locations [x;y;] ~exists (2:r2=1 /\ 3:r2=1) (* Condition is not very significant [causality more or less -> dd4] *) (* on doko we have: exists (2:r2=1 /\ 3:r2=2 /\ x=2 /\ y=1) *)