6 * This litmus test demonstrates that double-checked locking can be
7 * reliable given proper use of smp_load_acquire() and smp_store_release()
8 * in addition to the locking.
16 P0(int *flag, int *data, spinlock_t *lck)
22 r0 = smp_load_acquire(flag);
25 r1 = READ_ONCE(*flag);
28 smp_store_release(flag, 1);
32 r2 = READ_ONCE(*data);
35 P1(int *flag, int *data, spinlock_t *lck)
41 r0 = smp_load_acquire(flag);
44 r1 = READ_ONCE(*flag);
47 smp_store_release(flag, 1);
51 r2 = READ_ONCE(*data);
54 locations [flag;data;0:r0;0:r1;1:r0;1:r1]
55 exists (0:r2=0 \/ 1:r2=0)