LISA Alan07
(* Alan06 + some rs-critical section on P0 *)
{ }
P0 | P1 | P2 ;
f[rcu_read_lock] | r[once] r1 y | r[once] r2 z ;
w[once] x 1 | w[once] z r1 | f[rmb] ;
f[rcu_read_unlock]| | r[once] r3 x ;
f[wmb] | | ;
w[once] y 1 | | ;
Observed
2:r3=0; 2:r2=1; 1:r1=1;