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;