C C-rdw { int *x = &u; int *y = &u; } P0(int **x, int **y, int *z) { WRITE_ONCE(*z, 1); smp_mb(); WRITE_ONCE(*y, x); } P1(int **x, int **y) { int *r1; int r2; int *r3; int r4; r1 = lockless_dereference(*y); r2 = READ_ONCE(*r1); r3 = lockless_dereference(*x); r4 = READ_ONCE(*r3); } P2(int **x, int *z) { WRITE_ONCE(*x, z); } exists (1:r1=x /\ 1:r2=u /\ 1:r3=z /\ 1:r4=0)