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;