C DCL-fixed

(*
 * Result: Never
 *
 * This litmus test demonstrates that double-checked locking can be
 * reliable given proper use of smp_load_acquire() and smp_store_release()
 * in addition to the locking.
 *)

{
 int flag;
 int data;
}

P0(int *flag, int *data, spinlock_t *lck)
{
 int r0;
 int r1;
 int r2;

 r0 = smp_load_acquire(flag);
 if (r0 == 0) {
  spin_lock(lck);
  r1 = READ_ONCE(*flag);
  if (r1 == 0) {
   WRITE_ONCE(*data, 1);
   smp_store_release(flag, 1);
  }
  spin_unlock(lck);
 }
 r2 = READ_ONCE(*data);
}

P1(int *flag, int *data, spinlock_t *lck)
{
 int r0;
 int r1;
 int r2;

 r0 = smp_load_acquire(flag);
 if (r0 == 0) {
  spin_lock(lck);
  r1 = READ_ONCE(*flag);
  if (r1 == 0) {
   WRITE_ONCE(*data, 1);
   smp_store_release(flag, 1);
  }
  spin_unlock(lck);
 }
 r2 = READ_ONCE(*data);
}

locations [flag;data;0:r0;0:r1;1:r0;1:r1]
exists (0:r2=0 \/ 1:r2=0)