MP+porevlocks.litmus 765 B

1234567891011121314151617181920212223242526272829303132333435
  1. C MP+porevlocks
  2. (*
  3. * Result: Never
  4. *
  5. * This litmus test demonstrates how lock acquisitions and releases can
  6. * stand in for smp_load_acquire() and smp_store_release(), respectively.
  7. * In other words, when holding a given lock (or indeed after releasing a
  8. * given lock), a CPU is not only guaranteed to see the accesses that other
  9. * CPUs made while previously holding that lock, it is also guaranteed to
  10. * see all prior accesses by those other CPUs.
  11. *)
  12. {}
  13. P0(int *x, int *y, spinlock_t *mylock)
  14. {
  15. int r0;
  16. int r1;
  17. r0 = READ_ONCE(*y);
  18. spin_lock(mylock);
  19. r1 = READ_ONCE(*x);
  20. spin_unlock(mylock);
  21. }
  22. P1(int *x, int *y, spinlock_t *mylock)
  23. {
  24. spin_lock(mylock);
  25. WRITE_ONCE(*x, 1);
  26. spin_unlock(mylock);
  27. WRITE_ONCE(*y, 1);
  28. }
  29. exists (0:r0=1 /\ 0:r1=0)