|  | 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) |