tools/memory-model/litmus-tests/MP+polocks.litmus

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