C-RW-R+RW-R+RW-G+RW-G+RW-G+RW-G+RW-R+RW-R+RW-R+RW-R+RW-R+RW-R+RW-G+RW-G+RW-G+RW-G+RW-R+RW-R+RW-R.litmus

C auto/C-RW-R+RW-R+RW-G+RW-G+RW-G+RW-G+RW-R+RW-R+RW-R+RW-R+RW-R+RW-R+RW-G+RW-G+RW-G+RW-G+RW-R+RW-R+RW-R
(*
 * Result: Sometimes
 * 
 * Process 0 starts (t=491989).
 * 
 * P0 goes back a bit less than one grace period (t=392989).
 * 
 * P1 goes back a bit less than one grace period (t=293990).
 * 
 * P2 advances one grace period (t=393991).
 * 
 * P3 advances one grace period (t=493992).
 * 
 * P4 advances one grace period (t=593993).
 * 
 * P5 advances one grace period (t=693994).
 * 
 * P6 goes back a bit less than one grace period (t=594995).
 * 
 * P7 goes back a bit less than one grace period (t=495996).
 * 
 * P8 goes back a bit less than one grace period (t=396997).
 * 
 * P9 goes back a bit less than one grace period (t=297998).
 * 
 * P10 goes back a bit less than one grace period (t=198999).
 * 
 * P11 goes back a bit less than one grace period (t=100000).
 * 
 * P12 advances one grace period (t=200001).
 * 
 * P13 advances one grace period (t=300002).
 * 
 * P14 advances one grace period (t=400003).
 * 
 * P15 advances one grace period (t=500004).
 * 
 * P16 goes back a bit less than one grace period (t=401005).
 * 
 * P17 goes back a bit less than one grace period (t=302006).
 * 
 * P18 goes back a bit less than one grace period (t=203007).
 * 
 * Process 0 start at t=491989, process 19 end at t=203007: Cycle allowed.
 *)
{
}

P0(intptr_t *x0, intptr_t *x1)
{
	rcu_read_lock();
	intptr_t r1 = READ_ONCE(*x0);
	WRITE_ONCE(*x1, 1);
	rcu_read_unlock();
}


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


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


P3(intptr_t *x3, intptr_t *x4)
{
	intptr_t r1 = READ_ONCE(*x3);
	synchronize_rcu();
	WRITE_ONCE(*x4, 1);
}


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


P5(intptr_t *x5, intptr_t *x6)
{
	intptr_t r1 = READ_ONCE(*x5);
	synchronize_rcu();
	WRITE_ONCE(*x6, 1);
}


P6(intptr_t *x6, intptr_t *x7)
{
	rcu_read_lock();
	intptr_t r1 = READ_ONCE(*x6);
	WRITE_ONCE(*x7, 1);
	rcu_read_unlock();
}


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


P8(intptr_t *x8, intptr_t *x9)
{
	rcu_read_lock();
	intptr_t r1 = READ_ONCE(*x8);
	WRITE_ONCE(*x9, 1);
	rcu_read_unlock();
}


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


P10(intptr_t *x10, intptr_t *x11)
{
	rcu_read_lock();
	intptr_t r1 = READ_ONCE(*x10);
	WRITE_ONCE(*x11, 1);
	rcu_read_unlock();
}


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


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


P13(intptr_t *x13, intptr_t *x14)
{
	intptr_t r1 = READ_ONCE(*x13);
	synchronize_rcu();
	WRITE_ONCE(*x14, 1);
}


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


P15(intptr_t *x15, intptr_t *x16)
{
	intptr_t r1 = READ_ONCE(*x15);
	synchronize_rcu();
	WRITE_ONCE(*x16, 1);
}


P16(intptr_t *x16, intptr_t *x17)
{
	rcu_read_lock();
	intptr_t r1 = READ_ONCE(*x16);
	WRITE_ONCE(*x17, 1);
	rcu_read_unlock();
}


P17(intptr_t *x17, intptr_t *x18)
{
	rcu_read_lock();
	intptr_t r1 = READ_ONCE(*x17);
	WRITE_ONCE(*x18, 1);
	rcu_read_unlock();
}


P18(intptr_t *x18, intptr_t *x0)
{
	rcu_read_lock();
	intptr_t r1 = READ_ONCE(*x18);
	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 /\ 16:r1=1 /\ 17:r1=1 /\ 18:r1=1)