55 lines · plain
1C DCL-broken2 3(*4 * Result: Sometimes5 *6 * This litmus test demonstrates more than just locking is required to7 * correctly implement double-checked locking.8 *)9 10{11 int flag;12 int data;13}14 15P0(int *flag, int *data, spinlock_t *lck)16{17 int r0;18 int r1;19 int r2;20 21 r0 = READ_ONCE(*flag);22 if (r0 == 0) {23 spin_lock(lck);24 r1 = READ_ONCE(*flag);25 if (r1 == 0) {26 WRITE_ONCE(*data, 1);27 WRITE_ONCE(*flag, 1);28 }29 spin_unlock(lck);30 }31 r2 = READ_ONCE(*data);32}33 34P1(int *flag, int *data, spinlock_t *lck)35{36 int r0;37 int r1;38 int r2;39 40 r0 = READ_ONCE(*flag);41 if (r0 == 0) {42 spin_lock(lck);43 r1 = READ_ONCE(*flag);44 if (r1 == 0) {45 WRITE_ONCE(*data, 1);46 WRITE_ONCE(*flag, 1);47 }48 spin_unlock(lck);49 }50 r2 = READ_ONCE(*data);51}52 53locations [flag;data;0:r0;0:r1;1:r0;1:r1]54exists (0:r2=0 \/ 1:r2=0)55