LISA LISA3Rq1G (* * Result: Never * * One RCU grace period and three RCU read-side critical sections. * This would normally allow the cycle, but there is a release-acquire * relationship between P2's and P3's critical sections, which forces * P3's (but not P2's!) critical section to entirely follow the * grace period. Cycle prohibited. *) { x0 = 0; x1 = 0; x2 = 0; x3 = 0; v0 = 0; } P0 | P1 | P2 | P3 ; f[rcu_read_lock] | r[once] r1 x1 | f[rcu_read_lock] | f[rcu_read_lock] ; r[once] r2 x0 | f[sync] | r[once] r2 x2 | r[acquire] r3 x3 ; w[once] x1 1 | w[once] x2 1 | w[release] x3 1 | w[once] x0 1 ; f[rcu_read_unlock] | | f[rcu_read_unlock] | f[rcu_read_unlock] ; Observed 3:r3=1; 2:r2=1; 1:r1=0; 0:r2=1;