RCU+sync+free.litmus 892 B

123456789101112131415161718192021222324252627282930313233343536373839404142
  1. C RCU+sync+free
  2. (*
  3. * Result: Never
  4. *
  5. * This litmus test demonstrates that an RCU reader can never see a write that
  6. * follows a grace period, if it did not see writes that precede that grace
  7. * period.
  8. *
  9. * This is a typical pattern of RCU usage, where the write before the grace
  10. * period assigns a pointer, and the writes following the grace period destroy
  11. * the object that the pointer used to point to.
  12. *
  13. * This is one implication of the RCU grace-period guarantee, which says (among
  14. * other things) that an RCU read-side critical section cannot span a grace period.
  15. *)
  16. {
  17. int x = 1;
  18. int *y = &x;
  19. int z = 1;
  20. }
  21. P0(int *x, int *z, int **y)
  22. {
  23. int *r0;
  24. int r1;
  25. rcu_read_lock();
  26. r0 = rcu_dereference(*y);
  27. r1 = READ_ONCE(*r0);
  28. rcu_read_unlock();
  29. }
  30. P1(int *x, int *z, int **y)
  31. {
  32. rcu_assign_pointer(*y, z);
  33. synchronize_rcu();
  34. WRITE_ONCE(*x, 0);
  35. }
  36. exists (0:r0=x /\ 0:r1=0)