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
  16 P0(int *buf, int *flag, spinlock_t *mylock) // Producer
  17 {
  18         WRITE_ONCE(*buf, 1);
  19         spin_lock(mylock);
  20         WRITE_ONCE(*flag, 1);
  21         spin_unlock(mylock);
  22 }
  23
  24 P1(int *buf, int *flag, spinlock_t *mylock) // Consumer
  25 {
  26         int r0;
  27         int r1;
  28
  29         spin_lock(mylock);
  30         r0 = READ_ONCE(*flag);
  31         spin_unlock(mylock);
  32         r1 = READ_ONCE(*buf);
  33 }
  34
  35 exists (1:r0=1 /\ 1:r1=0) (* Bad outcome. *)