PPC m3l (mThreel) "write-to_read causality, boehm adve PLDI'08 (Fig 5.)" { P0:r5=x; P1:r5=x; P1:r6=y; P2:r5=x; P2:r6=y; P0:r1=1; P1:r1=1; } P0 | P1 | P2 ; stw r1,0,r5 | lwz r2,0,r5 | lwz r2,0,r6 ; | lwsync | lwsync ; | stw r1,0,r6 | lwz r1,0,r5 ; final (1:r2=1 /\ 2:r2=1 /\ 2:r1=0); with default: ~exists; (*PS: changed to ~exists to match model *) power_b: ~exists; doko: exists; (* SS: ?? I think *) (* According to boehm failure would reveal non-atomicity of writes *)