Test mcl

PPC mcl (PPCMTwelveLwSync)
{
x=0 ; y=0;
0:r4=x ; 0:r5=y;
1:r4=x ; 1:r5=y;
2:r4=x ; 2:r2=2 ;
3:r5=y ; 3:r1=1 ;
0:r1=1 ; 0:r2=2 ; 1:r3=3;
}

P0           |     P1       | P2           | P3          ;
stw r2,0(r5) | stw r3,0(r4) | stw r2,0(r4) |stw r1,0(r5) ;
lwsync       | sync         |              |             ;
stw r1,0(r4) | lwz r2,0(r5) |              |             ;


locations [1:r2; x; y;]
~exists (
(1:r2=0 /\ x=3 /\ y=1) \/
(1:r2=0 /\ x=3 /\ y=2) \/
(1:r2=1 /\ x=3 /\ y=2)
)