LISA Alan02
""
(*
Alan01 with wmb on P1 -> mb
*)
{
ok=1;
}
P0 | P1 | P2 ;
w[once] x 2 | w[once] y 2 | r[once] r0 z ;
f[wmb] | f[mb] | mov r1 (neq r0 1);
w[once] y 1 | w[once] z 1 | b[] r1 Fail ;
| | w[once] x 1 ;
| | b[] Exit ;
| |Fail: ;
| | w[once] ok 0 ;
| |Exit: ;
Observed
y=2; x=2; ok=1; 2:r0=1;