C auto/C-RR-R+WW-G
{
}


P0(int *x0, int *x1)
{
	rcu_read_lock();
	r1 = READ_ONCE(*x);
	r2 = READ_ONCE(*y);
	rcu_read_unlock();
}

P1(int *x0, int *x1)
{
	WRITE_ONCE(*y, 1);
	synchronize_rcu();
	WRITE_ONCE(*x, 1);
}

exists
(0:r1=1 /\ 0:r2=0)