C auto/C-RW-G+RW-R+RW-G+RW-R
(*
 * Result: Never
 * 
 * Process 0 starts (t=100000).
 * 
 * P0 advances one grace period (t=200000).
 * 
 * P1 goes back a bit less than one grace period (t=101001).
 * 
 * P2 advances one grace period (t=201002).
 * 
 * P3 goes back a bit less than one grace period (t=102003).
 * 
 * Process 0 start at t=100000, process 4 end at t=102003: Cycle forbidden.
 *)
{
}

P0(int *x0, int *x1)
{
	r1 = READ_ONCE(*x0);
	synchronize_rcu();
	WRITE_ONCE(*x1, 1);
}


P1(int *x1, int *x2)
{
	rcu_read_lock();
	r1 = READ_ONCE(*x1);
	WRITE_ONCE(*x2, 1);
	rcu_read_unlock();
}


P2(int *x2, int *x3)
{
	r1 = READ_ONCE(*x2);
	synchronize_rcu();
	WRITE_ONCE(*x3, 1);
}


P3(int *x0, int *x3)
{
	rcu_read_lock();
	r1 = READ_ONCE(*x3);
	WRITE_ONCE(*x0, 1);
	rcu_read_unlock();
}

exists
(0:r1=1 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=1)