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;