C auto/C-WW-H+WW-R+WW-R+WW-G+WW-R (* * Result: Never * * Process 0 starts (t=100000). * * P0 advances two grace periods (t=300000). * * P1 goes back a bit less than one grace period (t=201001). * * P2 goes back a bit less than one grace period (t=102002). * * P3 advances one grace period (t=202003). * * P4 goes back a bit less than one grace period (t=103004). * * Process 0 start at t=100000, process 5 end at t=103004: Cycle forbidden. *) { } P0(int *x0, int *x1) { WRITE_ONCE(*x0, 2); synchronize_rcu(); 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 *x0, int *x4) { rcu_read_lock(); WRITE_ONCE(*x4, 2); WRITE_ONCE(*x0, 1); rcu_read_unlock(); } Observed x4=1; x3=2; x2=2; x1=2; x0=2; and x4=2; x3=1; x2=2; x1=2; x0=2; and x4=1; x3=1; x2=2; x1=2; x0=2; and x4=2; x3=2; x2=1; x1=2; x0=2; and x4=1; x3=2; x2=1; x1=2; x0=2; and x4=2; x3=1; x2=1; x1=2; x0=2; and x4=1; x3=1; x2=1; x1=2; x0=2; and x4=2; x3=1; x2=2; x1=1; x0=2; and x4=2; x3=1; x2=1; x1=1; x0=2; and x4=2; x3=2; x2=2; x1=2; x0=1; and x4=1; x3=2; x2=2; x1=2; x0=1; and x4=2; x3=1; x2=2; x1=2; x0=1; and x4=1; x3=1; x2=2; x1=2; x0=1; and x4=2; x3=2; x2=1; x1=2; x0=1; and x4=1; x3=2; x2=1; x1=2; x0=1; and x4=2; x3=1; x2=1; x1=2; x0=1;