PPC ppc/nathan1 (PPCNathanOne)
{
P1:r1=1; P2:r1=1; P3:r1=1;
P0:r5=x; P1:r5=x; P2:r5=x; P3:r5=x;
P0:r6=y; P1:r6=y; P2:r6=y; P3:r6=y;
P0:r7=z; P1:r7=z; P2:r7=z; P3:r7=z;
x = 0; y = 0; z=0;
}
P0 | P1 | P2 | P3 ;
| | | ;
lwz r8,0(r5) | stw r1,0(r6) | stw r1,0(r7) | lwz r8,0(r7) ;
mr r12,r8 | lwz r8,0(r6) | | sync ;
xor r12,r12,r12 | mr r12,r8 | | stw r1,0(r5) ;
lwzx r9,r12,r6 | xor r12,r12,r12 | | ;
| lwzx r9,r12,r7 | | ;
exists (P0:r8=1 /\ P0:r9 = 0 /\ P1:r8=1 /\ P1:r9=0 /\ P3:r8 = 1);
<<
show 0
genprog generated/ppc-nathan1-prog.tex
essdump generated/ppc-nathan1-ess.dot
>>
<<
show 0
show interesting true
readfrom generated/ppc-nathan1-rf.dot
>>