LISA ISA2+rl-o-o-rul+rl-o-o-rul+o-srcu-o (* Allowed: More RCU RS CSes than GPs. *) { a = 1; x = 2; c = 0; } P0 | P1 | P2 ; f[rcu_read_lock] | f[rcu_read_lock] | ; w[once] a 3 | r[once] r1 x | r[once] r3 c ; | | f[sync] ; w[once] x 4 | w[once] c 1 | r[once] r2 a ; f[rcu_read_unlock] | f[rcu_read_unlock] | ; Observed 2:r3=1; 2:r2=1; 1:r1=4;