0001 C RCU+sync+free
0002
0003 (*
0004 * Result: Never
0005 *
0006 * This litmus test demonstrates that an RCU reader can never see a write that
0007 * follows a grace period, if it did not see writes that precede that grace
0008 * period.
0009 *
0010 * This is a typical pattern of RCU usage, where the write before the grace
0011 * period assigns a pointer, and the writes following the grace period destroy
0012 * the object that the pointer used to point to.
0013 *
0014 * This is one implication of the RCU grace-period guarantee, which says (among
0015 * other things) that an RCU read-side critical section cannot span a grace period.
0016 *)
0017
0018 {
0019 int x = 1;
0020 int *y = &x;
0021 int z = 1;
0022 }
0023
0024 P0(int *x, int *z, int **y)
0025 {
0026 int *r0;
0027 int r1;
0028
0029 rcu_read_lock();
0030 r0 = rcu_dereference(*y);
0031 r1 = READ_ONCE(*r0);
0032 rcu_read_unlock();
0033 }
0034
0035 P1(int *x, int *z, int **y)
0036 {
0037 rcu_assign_pointer(*y, z);
0038 synchronize_rcu();
0039 WRITE_ONCE(*x, 0);
0040 }
0041
0042 exists (0:r0=x /\ 0:r1=0)
