C-RW-R+RW-R+RW-G+RW-G+RW-G+RW-G+RW-R+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
(*
 * Result: Sometimes
 * 
 * Process 0 starts (t=297999).
 * 
 * P0 goes back a bit less than one grace period (t=198999).
 * 
 * P1 goes back a bit less than one grace period (t=100000).
 * 
 * P2 advances one grace period (t=200001).
 * 
 * P3 advances one grace period (t=300002).
 * 
 * P4 advances one grace period (t=400003).
 * 
 * P5 advances one grace period (t=500004).
 * 
 * P6 goes back a bit less than one grace period (t=401005).
 * 
 * P7 goes back a bit less than one grace period (t=302006).
 * 
 * P8 goes back a bit less than one grace period (t=203007).
 * 
 * P9 goes back a bit less than one grace period (t=104008).
 * 
 * Process 0 start at t=297999, process 10 end at t=104008: 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 *x0)
{
	rcu_read_lock();
	intptr_t r1 = READ_ONCE(*x9);
	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)