MP+onceassign+derefonce.litmus 593 B

123456789101112131415161718192021222324252627282930313233
  1. C MP+onceassign+derefonce
  2. (*
  3. * Result: Never
  4. *
  5. * This litmus test demonstrates that rcu_assign_pointer() and
  6. * rcu_dereference() suffice to ensure that an RCU reader will not see
  7. * pre-initialization garbage when it traverses an RCU-protected data
  8. * structure containing a newly inserted element.
  9. *)
  10. {
  11. p=y;
  12. }
  13. P0(int *x, int **p) // Producer
  14. {
  15. WRITE_ONCE(*x, 1);
  16. rcu_assign_pointer(*p, x);
  17. }
  18. P1(int *x, int **p) // Consumer
  19. {
  20. int *r0;
  21. int r1;
  22. rcu_read_lock();
  23. r0 = rcu_dereference(*p);
  24. r1 = READ_ONCE(*r0);
  25. rcu_read_unlock();
  26. }
  27. exists (1:r0=x /\ 1:r1=0) (* Bad outcome. *)