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

C auto/C-WW-G+WW-G+WW-G+WW-B+WW-R+WW-R
(*
 * Result: Never
 * 
 * Process 0 starts (t=100000).
 * 
 * P0 advances one grace period (t=200000).
 * 
 * P1 advances one grace period (t=300001).
 * 
 * P2 advances one grace period (t=400002).
 * 
 * P3 advances slightly (t=400004).
 * 
 * P4 goes back a bit less than one grace period (t=301005).
 * 
 * P5 goes back a bit less than one grace period (t=202006).
 * 
 * Process 0 start at t=100000, process 6 end at t=202006: Cycle forbidden.
 *)
{
}

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


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


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


P3(int *x3, int *x4)
{
 WRITE_ONCE(*x3, 2);
 smp_mb();
 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=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=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=2; x2=2; x1=1; x0=2;
and x5=1; x4=2; x3=2; x2=2; x1=1; x0=2;
and x5=2; x4=1; x3=2; x2=2; x1=1; x0=2;
and x5=1; x4=1; x3=2; x2=2; x1=1; x0=2;
and x5=2; x4=2; x3=2; x2=1; x1=1; x0=2;
and x5=1; x4=2; x3=2; x2=1; x1=1; x0=2;
and x5=2; x4=1; x3=2; x2=1; x1=1; x0=2;
and x5=1; x4=1; x3=2; 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=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=2; x4=1; x3=2; x2=1; x1=2; x0=1;
and x5=1; x4=1; x3=2; x2=1; x1=2; x0=1;
and x5=1; x4=2; 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=1; x4=2; x3=2; x2=2; x1=1; x0=1;
and x5=2; x4=1; x3=2; x2=2; x1=1; x0=1;
and x5=1; x4=1; x3=2; x2=2; x1=1; x0=1;
and x5=1; x4=2; x3=1; x2=2; x1=1; x0=1;
and x5=2; x4=1; x3=1; x2=2; x1=1; x0=1;
and x5=1; x4=1; x3=1; x2=2; x1=1; x0=1;
and x5=2; x4=2; x3=2; x2=1; x1=1; x0=1;
and x5=1; x4=2; x3=2; x2=1; x1=1; x0=1;
and x5=1; x4=1; x3=2; x2=1; x1=1; x0=1;