LISA MP+o-rmb-o+o-mb-o (* Allow, rmb orders only reads. *) { x = 0; y = 0; } P0 | P1 ; w[once] y 1 | r[once] r1 x ; f[rmb] | f[mb] ; w[once] x 1 | r[once] r2 y ; Observed 1:r2=0; 1:r1=1;