56 lines · plain
1C DCL-fixed2 3(*4 * Result: Never5 *6 * This litmus test demonstrates that double-checked locking can be7 * reliable given proper use of smp_load_acquire() and smp_store_release()8 * in addition to the locking.9 *)10 11{12 int flag;13 int data;14}15 16P0(int *flag, int *data, spinlock_t *lck)17{18 int r0;19 int r1;20 int r2;21 22 r0 = smp_load_acquire(flag);23 if (r0 == 0) {24 spin_lock(lck);25 r1 = READ_ONCE(*flag);26 if (r1 == 0) {27 WRITE_ONCE(*data, 1);28 smp_store_release(flag, 1);29 }30 spin_unlock(lck);31 }32 r2 = READ_ONCE(*data);33}34 35P1(int *flag, int *data, spinlock_t *lck)36{37 int r0;38 int r1;39 int r2;40 41 r0 = smp_load_acquire(flag);42 if (r0 == 0) {43 spin_lock(lck);44 r1 = READ_ONCE(*flag);45 if (r1 == 0) {46 WRITE_ONCE(*data, 1);47 smp_store_release(flag, 1);48 }49 spin_unlock(lck);50 }51 r2 = READ_ONCE(*data);52}53 54locations [flag;data;0:r0;0:r1;1:r0;1:r1]55exists (0:r2=0 \/ 1:r2=0)56