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)