LISA Weak-RCU-Readers (*Paul says allowed*)
{
x = 0; y = 0;
}
P0 | P1 ;
f[rcu_read_lock] | f[rcu_read_lock] ;
r[once] r1 x | r[once] r2 y ;
f[rcu_read_unlock] | f[rcu_read_unlock] ;
f[rcu_read_lock] | f[rcu_read_lock] ;
w[once] y 1 | w[once] x 1 ;
f[rcu_read_unlock] | f[rcu_read_unlock] ;
Observed
1:r2=1; 0:r1=1;