34 lines · plain
1C MP+onceassign+derefonce2 3(*4 * Result: Never5 *6 * This litmus test demonstrates that rcu_assign_pointer() and7 * rcu_dereference() suffice to ensure that an RCU reader will not see8 * pre-initialization garbage when it traverses an RCU-protected data9 * structure containing a newly inserted element.10 *)11 12{13p=y;14}15 16P0(int *x, int **p) // Producer17{18 WRITE_ONCE(*x, 1);19 rcu_assign_pointer(*p, x);20}21 22P1(int *x, int **p) // Consumer23{24 int *r0;25 int r1;26 27 rcu_read_lock();28 r0 = rcu_dereference(*p);29 r1 = READ_ONCE(*r0);30 rcu_read_unlock();31}32 33exists (1:r0=x /\ 1:r1=0) (* Bad outcome. *)34