LISA RCU-idempotency { } P0 | P1 | P2 ; f[rcu_read_lock] | w[once] x 1 | f[rcu_read_lock] ; r[once] r0 x | f[sync] | r[once] r0 z ; r[once] r1 y | w[once] z 1 | w[once] y 1 ; f[rcu_read_unlock] | | f[rcu_read_unlock] ; Observed 2:r0=1; 0:r1=1; 0:r0=0;