1C DCL-fixed 2 3(* 4 * Result: Never 5 * 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. 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