C C-LB+o-rel+rl-o-o-rul+o-sync-o.litmus { } P0(int *a, int *r) { int r1; r1 = READ_ONCE(*a); smp_store_release(r, 1); } P1(int *b, int *a) { int r2; rcu_read_lock(); r2 = READ_ONCE(*b); WRITE_ONCE(*a, 1); rcu_read_unlock(); } P2(int *r, int *b) { int r1; r1 = READ_ONCE(*r); synchronize_rcu(); WRITE_ONCE(*b, 1); } filter (2:r1=1) exists (0:r1=1 /\ 1:r2=1)