| C RCU+sync+read |
| |
| (* |
| * Result: Never |
| * |
| * This litmus test demonstrates that after a grace period, an RCU updater always |
| * sees all stores done in prior RCU read-side critical sections. Such |
| * read-side critical sections would have ended before the grace period ended. |
| * |
| * This is one implication of the RCU grace-period guarantee, which says (among |
| * other things) that an RCU read-side critical section cannot span a grace period. |
| *) |
| |
| { |
| int x = 0; |
| int y = 0; |
| } |
| |
| P0(int *x, int *y) |
| { |
| rcu_read_lock(); |
| WRITE_ONCE(*x, 1); |
| WRITE_ONCE(*y, 1); |
| rcu_read_unlock(); |
| } |
| |
| P1(int *x, int *y) |
| { |
| int r0; |
| int r1; |
| |
| r0 = READ_ONCE(*x); |
| synchronize_rcu(); |
| r1 = READ_ONCE(*y); |
| } |
| |
| exists (1:r0=1 /\ 1:r1=0) |