C C-MP+o-assign+ldref-o.litmus { x=y0; 0:r4=y; } P0(int *x, int *y) { WRITE_ONCE(*y, 1); rcu_assign_pointer(*x, r4); } P1(int *x, int *y) { int r1; int r2; r1 = lockless_dereference(*x); r2 = READ_ONCE(*r1); } exists (1:r1=y /\ 1:r2=0)