R+fencembonceonces.litmus 499 B

123456789101112131415161718192021222324252627282930
  1. C R+fencembonceonces
  2. (*
  3. * Result: Never
  4. *
  5. * This is the fully ordered (via smp_mb()) version of one of the classic
  6. * counterintuitive litmus tests that illustrates the effects of store
  7. * propagation delays. Note that weakening either of the barriers would
  8. * cause the resulting test to be allowed.
  9. *)
  10. {}
  11. P0(int *x, int *y)
  12. {
  13. WRITE_ONCE(*x, 1);
  14. smp_mb();
  15. WRITE_ONCE(*y, 1);
  16. }
  17. P1(int *x, int *y)
  18. {
  19. int r0;
  20. WRITE_ONCE(*y, 2);
  21. smp_mb();
  22. r0 = READ_ONCE(*x);
  23. }
  24. exists (y=2 /\ 1:r0=0)