Test auto/C-WW-G+WW-R+WW-R+WW-G+WW-R+WW-R

C auto/C-WW-G+WW-R+WW-R+WW-G+WW-R+WW-R
(*
 * Result: Sometimes
 * 
 * Process 0 starts (t=295995).
 * 
 * P0 advances one grace period (t=395995).
 * 
 * P1 goes back a bit less than one grace period (t=296996).
 * 
 * P2 goes back a bit less than one grace period (t=197997).
 * 
 * P3 advances one grace period (t=297998).
 * 
 * P4 goes back a bit less than one grace period (t=198999).
 * 
 * P5 goes back a bit less than one grace period (t=100000).
 * 
 * Process 0 start at t=295995, process 6 end at t=100000: Cycle allowed.
 *)
{
}

P0(int *x0, int *x1)
{
 WRITE_ONCE(*x0, 2);
 synchronize_rcu();
 WRITE_ONCE(*x1, 1);
}


P1(int *x1, int *x2)
{
 rcu_read_lock();
 WRITE_ONCE(*x1, 2);
 WRITE_ONCE(*x2, 1);
 rcu_read_unlock();
}


P2(int *x2, int *x3)
{
 rcu_read_lock();
 WRITE_ONCE(*x2, 2);
 WRITE_ONCE(*x3, 1);
 rcu_read_unlock();
}


P3(int *x3, int *x4)
{
 WRITE_ONCE(*x3, 2);
 synchronize_rcu();
 WRITE_ONCE(*x4, 1);
}


P4(int *x4, int *x5)
{
 rcu_read_lock();
 WRITE_ONCE(*x4, 2);
 WRITE_ONCE(*x5, 1);
 rcu_read_unlock();
}


P5(int *x0, int *x5)
{
 rcu_read_lock();
 WRITE_ONCE(*x5, 2);
 WRITE_ONCE(*x0, 1);
 rcu_read_unlock();
}

Observed
    x5=2; x4=2; x3=2; x2=2; x1=2; x0=2;
and x5=1; x4=2; x3=2; x2=2; x1=2; x0=2;
and x5=2; x4=1; x3=2; x2=2; x1=2; x0=2;
and x5=1; x4=1; x3=2; x2=2; x1=2; x0=2;
and x5=2; x4=2; x3=1; x2=2; x1=2; x0=2;
and x5=1; x4=2; x3=1; x2=2; x1=2; x0=2;
and x5=2; x4=1; x3=1; x2=2; x1=2; x0=2;
and x5=1; x4=1; x3=1; x2=2; x1=2; x0=2;
and x5=2; x4=2; x3=2; x2=1; x1=2; x0=2;
and x5=1; x4=2; x3=2; x2=1; x1=2; x0=2;
and x5=1; x4=1; x3=2; x2=1; x1=2; x0=2;
and x5=2; x4=2; x3=1; x2=1; x1=2; x0=2;
and x5=1; x4=2; x3=1; x2=1; x1=2; x0=2;
and x5=2; x4=1; x3=1; x2=1; x1=2; x0=2;
and x5=1; x4=1; x3=1; x2=1; x1=2; x0=2;
and x5=2; x4=2; x3=2; x2=2; x1=1; x0=2;
and x5=2; x4=2; x3=1; x2=2; x1=1; x0=2;
and x5=1; x4=2; x3=1; x2=2; x1=1; x0=2;
and x5=2; x4=2; x3=2; x2=1; x1=1; x0=2;
and x5=2; x4=2; x3=1; x2=1; x1=1; x0=2;
and x5=1; x4=2; x3=1; x2=1; x1=1; x0=2;
and x5=2; x4=2; x3=2; x2=2; x1=2; x0=1;
and x5=1; x4=2; x3=2; x2=2; x1=2; x0=1;
and x5=2; x4=1; x3=2; x2=2; x1=2; x0=1;
and x5=1; x4=1; x3=2; x2=2; x1=2; x0=1;
and x5=2; x4=2; x3=1; x2=2; x1=2; x0=1;
and x5=1; x4=2; x3=1; x2=2; x1=2; x0=1;
and x5=2; x4=1; x3=1; x2=2; x1=2; x0=1;
and x5=1; x4=1; x3=1; x2=2; x1=2; x0=1;
and x5=2; x4=2; x3=2; x2=1; x1=2; x0=1;
and x5=1; x4=2; x3=2; x2=1; x1=2; x0=1;
and x5=1; x4=1; x3=2; x2=1; x1=2; x0=1;
and x5=2; x4=2; x3=1; x2=1; x1=2; x0=1;
and x5=1; x4=2; x3=1; x2=1; x1=2; x0=1;
and x5=2; x4=1; x3=1; x2=1; x1=2; x0=1;
and x5=1; x4=1; x3=1; x2=1; x1=2; x0=1;
and x5=2; x4=2; x3=2; x2=2; x1=1; x0=1;
and x5=2; x4=2; x3=1; x2=2; x1=1; x0=1;
and x5=1; x4=2; x3=1; x2=2; x1=1; x0=1;
and x5=2; x4=2; x3=2; x2=1; x1=1; x0=1;
and x5=2; x4=2; x3=1; x2=1; x1=1; x0=1;
and x5=1; x4=2; x3=1; x2=1; x1=1; x0=1;