C auto/C-RW-G+RW-R+RW-G+RW-R+RW-G+RW-R+RW-G+RW-R+RW-G+RW-R+RW-G+RW-R+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).
 * 
 * P4 advances one grace period (t=202004).
 * 
 * P5 goes back a bit less than one grace period (t=103005).
 * 
 * P6 advances one grace period (t=203006).
 * 
 * P7 goes back a bit less than one grace period (t=104007).
 * 
 * P8 advances one grace period (t=204008).
 * 
 * P9 goes back a bit less than one grace period (t=105009).
 * 
 * P10 advances one grace period (t=205010).
 * 
 * P11 goes back a bit less than one grace period (t=106011).
 * 
 * P12 advances one grace period (t=206012).
 * 
 * P13 goes back a bit less than one grace period (t=107013).
 * 
 * P14 advances one grace period (t=207014).
 * 
 * P15 goes back a bit less than one grace period (t=108015).
 * 
 * Process 0 start at t=100000, process 16 end at t=108015: 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 *x3, int *x4)
{
	rcu_read_lock();
	r1 = READ_ONCE(*x3);
	WRITE_ONCE(*x4, 1);
	rcu_read_unlock();
}


P4(int *x4, int *x5)
{
	r1 = READ_ONCE(*x4);
	synchronize_rcu();
	WRITE_ONCE(*x5, 1);
}


P5(int *x5, int *x6)
{
	rcu_read_lock();
	r1 = READ_ONCE(*x5);
	WRITE_ONCE(*x6, 1);
	rcu_read_unlock();
}


P6(int *x6, int *x7)
{
	r1 = READ_ONCE(*x6);
	synchronize_rcu();
	WRITE_ONCE(*x7, 1);
}


P7(int *x7, int *x8)
{
	rcu_read_lock();
	r1 = READ_ONCE(*x7);
	WRITE_ONCE(*x8, 1);
	rcu_read_unlock();
}


P8(int *x8, int *x9)
{
	r1 = READ_ONCE(*x8);
	synchronize_rcu();
	WRITE_ONCE(*x9, 1);
}


P9(int *x9, int *x10)
{
	rcu_read_lock();
	r1 = READ_ONCE(*x9);
	WRITE_ONCE(*x10, 1);
	rcu_read_unlock();
}


P10(int *x10, int *x11)
{
	r1 = READ_ONCE(*x10);
	synchronize_rcu();
	WRITE_ONCE(*x11, 1);
}


P11(int *x11, int *x12)
{
	rcu_read_lock();
	r1 = READ_ONCE(*x11);
	WRITE_ONCE(*x12, 1);
	rcu_read_unlock();
}


P12(int *x12, int *x13)
{
	r1 = READ_ONCE(*x12);
	synchronize_rcu();
	WRITE_ONCE(*x13, 1);
}


P13(int *x13, int *x14)
{
	rcu_read_lock();
	r1 = READ_ONCE(*x13);
	WRITE_ONCE(*x14, 1);
	rcu_read_unlock();
}


P14(int *x14, int *x15)
{
	r1 = READ_ONCE(*x14);
	synchronize_rcu();
	WRITE_ONCE(*x15, 1);
}


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

exists
(0:r1=1 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 4:r1=1 /\ 5:r1=1 /\ 6:r1=1 /\ 7:r1=1 /\ 8:r1=1 /\ 9:r1=1 /\ 10:r1=1 /\ 11:r1=1 /\ 12:r1=1 /\ 13:r1=1 /\ 14:r1=1 /\ 15:r1=1)