PPC ppc-cpp.rwc.nobarrier (PPCcppRWCNoBarrier) "read-to-write causality, boehm adve PLDI'08 (Fig 6.)" { P0:r1=x; P1:r1=x; P1:r2=y; P2:r1=x; P2:r2=y; P0:r0=1; P2:r0=1; } P0 | P1 | P2 ; stw r0,0,r1 | lwz r5,0,r1 | stw r0,0,r2 ; | lwz r6,0,r2 | lwz r7,0,r1 ; exists (P1:r5=1 /\ P1:r6=0 /\ P2:r7=0) << genprog generated/ppc-cpp.rwc.nobarrier-prog.tex show 1 essdump generated/ppc-cpp.rwc.nobarrier-ess.dot >> << show 0 of ess 0 show interesting true readfrom generated/ppc-cpp.rwc.nobarrier-rf.dot >>