LISA auto/RW-G+RW-R2I (* * Result: Sometimes * * Process 0 starts (t=100000). * * P0 advances one grace period (t=200000). * * P1 is unordered, therefore cycle is allowed. * Skipping remainder of analysis. *) { } P0 | P1 ; r[once] r1 x0 | w[once] x0 1 ; f[sync] | f[rcu_read_lock] ; w[once] x1 1 | r[once] r1 x1 ; | f[rcu_read_unlock] ; Observed 1:r1=1; 0:r1=1;