C auto/C-WW-R+WW-R+WW-R+WW-R+WW-R+WW-R
(*
* Result: Sometimes
*
* Process 0 starts (t=693995).
*
* P0 goes back a bit less than one grace period (t=594995).
*
* P1 goes back a bit less than one grace period (t=495996).
*
* P2 goes back a bit less than one grace period (t=396997).
*
* P3 goes back a bit less than 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=693995, process 6 end at t=100000: Cycle allowed.
*)
{
}
P0(int *x0, int *x1)
{
rcu_read_lock();
WRITE_ONCE(*x0, 2);
WRITE_ONCE(*x1, 1);
rcu_read_unlock();
}
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)
{
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;