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

   1 C MP+porevlocks
   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 to
  11  * 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) // Consumer
  21 {
  22         int r0;
  23         int r1;
  24
  25         r0 = READ_ONCE(*flag);
  26         spin_lock(mylock);
  27         r1 = READ_ONCE(*buf);
  28         spin_unlock(mylock);
  29 }
  30
  31 P1(int *buf, int *flag, spinlock_t *mylock) // Producer
  32 {
  33         spin_lock(mylock);
  34         WRITE_ONCE(*buf, 1);
  35         spin_unlock(mylock);
  36         WRITE_ONCE(*flag, 1);
  37 }
  38
  39 exists (0:r0=1 /\ 0:r1=0) (* Bad outcome. *)