…
C auto/C-WW-G+WW-R+WW-R+WW-R+WW-G+WW-R
(*
* Result: Sometimes
*
* Process 0 starts (t=296997).
*
* P0 advances one grace period (t=396997).
*
* P1 goes back a bit less than one grace period (t=297998).
*
* P2 goes back a bit less than one grace period (t=198999).
*
* P3 goes back a bit less than one grace period (t=100000).
*
* P4 advances one grace period (t=200001).
*
* P5 goes back a bit less than one grace period (t=101002).
*
* Process 0 start at t=296997, process 6 end at t=101002: 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)
{
rcu_read_lock();
WRITE_ONCE(*x3, 2);
WRITE_ONCE(*x4, 1);
rcu_read_unlock();
}
P4(int *x4, int *x5)
{
WRITE_ONCE(*x4, 2);
synchronize_rcu();
WRITE_ONCE(*x5, 1);
}
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=2; x4=1; 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=1; x3=2; x2=2; x1=1; x0=2;
and x5=2; x4=1; 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=1; x3=2; x2=1; x1=1; x0=2;
and x5=2; x4=2; x3=1; x2=1; x1=1; x0=2;
and x5=2; x4=1; 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=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=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=1; x3=1; x2=1; x1=1; x0=1;