| * This litmus test demonstrates how lock acquisitions and releases can |
| * stand in for smp_load_acquire() and smp_store_release(), respectively. |
| * In other words, when holding a given lock (or indeed after releasing a |
| * given lock), a CPU is not only guaranteed to see the accesses that other |
| * CPUs made while previously holding that lock, it is also guaranteed to |
| * see all prior accesses by those other CPUs. |
| P0(int *buf, int *flag, spinlock_t *mylock) // Consumer |
| P1(int *buf, int *flag, spinlock_t *mylock) // Producer |
| exists (0:r0=1 /\ 0:r1=0) (* Bad outcome. *) |