LISA LISA2Rfi1G (* * Result: Sometimes * * One RCU grace period and two RCU read-side critical sections, which * would normally allow the cycle. P2's RCU read-side critical section * contains a memory barrier, however, this memory barrier is not * positioned so as to force the critical section to entirely follow * the grace period. Cycle allowed. *) { x0 = 0; x1 = 0; x2 = 0; } P0 | P1 | P2 ; f[rcu_read_lock] | r[once] r1 x1 | f[rcu_read_lock] ; r[once] r2 x0 | f[sync] | w[once] x0 1 ; w[once] x1 1 | w[once] x2 1 | f[mb] ; f[rcu_read_unlock] | | r[once] r2 x2 ; | | f[rcu_read_unlock] ; Observed 2:r2=1; 1:r1=1; 0:r2=1;