LISA ISA2+o-rel+acq-o+o-rb-o { a = 1; x = 2; } P0 | P1 | P2; w[once] a 3 | r[acquire] r1 x | r[once] r3 c ; | | f[rmb] ; w[release] x 4 | w[once] c 1 | r[once] r2 a ; Observed 2:r3=1; 2:r2=1; 1:r1=4;