LISA WWC+o-branch-o+o-branch-o (* Allowed: Control dependencies not transitive. Also allowed by PowerPC. *) { x = 0; y = 0; } P0 | P1 | P2 ; r[once] r1 x | r[once] r2 y | w[once] x 2 ; mov r3 (eq r1 0) | mov r4 (eq r2 0) | ; b[] r3 END1 | b[] r4 END2 | ; w[once] y 1 | w[once] x 1 | ; END1: | END2: | ; Observed x=2; 1:r2=1; 0:r1=2;