
PPC mal (PPCMTenLwSync)
" ST ; LD || LD ; ST hexa version"
{
P0:r4=x ; P0:r5=y ; P0:r1=1 ;
P1:r4=x ; P1:r5=y ; P1:r1=2 ;
P2:r4=x ; P3:r5=y ;
P3:r2=2 ;
}
P0 |P1 |P2 |P3 ;
stw r1,0(r4) |lwz r2,0(r5) | | ;
sync |lwsync | | ;
lwz r2,0(r5) |stw r1,0(r4) |lwz r1,0(r4) |stw r2,0(r5) ;
locations [0:r2 ; 1:r2 ; 2:r1 ; x ;]
exists
(
(0:r2=0 /\ 1:r2=2 /\ 2:r1=1 /\ x=1) \/
(0:r2 =0 /\ 1:r2=2 /\ 2:r1=2 /\ x=1) \/
(0:r2 =0 /\ 1:r2=2 /\ 2:r1=0 /\ x=1)
)