36 lines · plain
1C MP+polocks2 3(*4 * Result: Never5 *6 * This litmus test demonstrates how lock acquisitions and releases can7 * stand in for smp_load_acquire() and smp_store_release(), respectively.8 * In other words, when holding a given lock (or indeed after releasing a9 * given lock), a CPU is not only guaranteed to see the accesses that other10 * CPUs made while previously holding that lock, it is also guaranteed11 * to see all prior accesses by those other CPUs.12 *)13 14{}15 16P0(int *buf, int *flag, spinlock_t *mylock) // Producer17{18 WRITE_ONCE(*buf, 1);19 spin_lock(mylock);20 WRITE_ONCE(*flag, 1);21 spin_unlock(mylock);22}23 24P1(int *buf, int *flag, spinlock_t *mylock) // Consumer25{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 35exists (1:r0=1 /\ 1:r1=0) (* Bad outcome. *)36