C auto/C-RW-G+RW-R+RW-G+RW-R+RW-G+RW-R (* * Result: Never * * Process 0 starts (t=100000). * * P0 advances one grace period (t=200000). * * P1 goes back a bit less than one grace period (t=101001). * * P2 advances one grace period (t=201002). * * P3 goes back a bit less than one grace period (t=102003). * * P4 advances one grace period (t=202004). * * P5 goes back a bit less than one grace period (t=103005). * * Process 0 start at t=100000, process 6 end at t=103005: Cycle forbidden. *) { } P0(int *x0, int *x1) { r1 = READ_ONCE(*x0); synchronize_rcu(); WRITE_ONCE(*x1, 1); } P1(int *x1, int *x2) { rcu_read_lock(); r1 = READ_ONCE(*x1); WRITE_ONCE(*x2, 1); rcu_read_unlock(); } P2(int *x2, int *x3) { r1 = READ_ONCE(*x2); synchronize_rcu(); WRITE_ONCE(*x3, 1); } P3(int *x3, int *x4) { rcu_read_lock(); r1 = READ_ONCE(*x3); WRITE_ONCE(*x4, 1); rcu_read_unlock(); } P4(int *x4, int *x5) { r1 = READ_ONCE(*x4); synchronize_rcu(); WRITE_ONCE(*x5, 1); } P5(int *x0, int *x5) { rcu_read_lock(); r1 = READ_ONCE(*x5); WRITE_ONCE(*x0, 1); rcu_read_unlock(); } exists (0:r1=1 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 4:r1=1 /\ 5:r1=1)