LISA IRIW+rl-o-o-rul+o-srcu-o (lwn.net/Articles/573497/0-RCU)
(*
* Forbid: Implicit full barrier between end of P0 and P1's read from x.
* This invokes something resembling A cumulativity.
*)
{
x = 0;
y = 0;
}
P0 | P1 | P2 | P3 ;
f[rcu_read_lock] | | | ;
r[once] r1 x | r[once] r3 y | w[once] x 1 | w[once] y 1 ;
| f[sync] | | ;
r[once] r2 y | r[once] r4 x | | ;
f[rcu_read_unlock] | | | ;
Observed
1:r4=0; 1:r3=1; 0:r2=1; 0:r1=1;
and 1:r4=0; 1:r3=0; 0:r2=0; 0:r1=1;