LISA rcu-relacq2
""
{
}
P0 | P1 | P2 ;
r[once] r0 x | w[once] y 2 | w[once] u 1 ;
w[once] y r0 | f[sync] | w[release] x 1 ;
f[rcu_read_lock] | w[once] v 1 | ;
r[once] r1 u | | ;
r[once] r2 v | | ;
f[rcu_read_unlock] | | ;
Observed
y=2; 0:r2=1; 0:r1=1; 0:r0=1;
and y=1; 0:r2=1; 0:r1=0; 0:r0=1;
and y=1; 0:r2=0; 0:r1=0; 0:r0=1;
and y=2; 0:r2=1; 0:r1=1; 0:r0=0;
and y=2; 0:r2=1; 0:r1=0; 0:r0=0;