PPC ccv4 (CCFour) "Boehm/adve CC example (Fig.8), sync" { 0:r1=1 ; 0:r5=x; 1:r5=x ; 1:r6=y; 2:r5=x ; 2:r6=y; 2:r1=1; 2:r2=2; 3:r5=x ; } P0 |P1 |P2 |P3 ; stw r1,0(r5)|lwz r1,0(r5)|stw r1,0(r6)|lwz r1,0(r5); |sync |sync |sync ; |lwz r2,0(r6)|stw r2,0(r5)|lwz r2,0(r5); (* Must be seq const. *) locations [x; 3:r1; 3:r2] ~exists (1:r1=1 /\ 1:r2=0 /\ x=1 )