非seq_cstメモリアクセスあれこれメモ

4スレッド/非SC実行での振る舞い

int main() {
  atomic_int x = 0;
  atomic_int y = 0;
  {{{ { y.store(1, memory_order_release); }
  ||| { x.store(1, memory_order_release); }
  ||| { r0 = x.load(memory_order_acquire).readsvalue(0);
        r1 = y.load(memory_order_acquire).readsvalue(1); }
  ||| { r2 = x.load(memory_order_acquire).readsvalue(1);
        r3 = y.load(memory_order_acquire).readsvalue(0); }
  }}}
  return 0;
}
// 4 executions; 1 consistent, race free

2スレッド/非SC実行での振る舞い（4スレッド版からの簡約）

int main() {
  atomic_int x = 0;
  atomic_int y = 0;
  {{{ { y.store(1, memory_order_release);
        r1 = x.load(memory_order_acquire).readsvalue(0); }
  ||| { x.store(1, memory_order_release);
        r2 = y.load(memory_order_acquire).readsvalue(0); }
  }}}
  return 0;
}
// 4 executions; 1 consistent, race free

rel-acq関係/遷移的HB(SW)

int main() {
  int g = 0;
  atomic_int x = 0;
  atomic_int y = 0;
  {{{ { g = 1;
        x.store(1, memory_order_release); }
  ||| { r0 = x.load(memory_order_acquire).readsvalue(1);
        y.store(1, memory_order_release); }
  ||| { r1 = y.load(memory_order_acquire).readsvalue(1);
        r2 = g; }
  }}}
  return 0;
}
// 8 executions; 1 consistent, race free

rel-con+rel-acq関係/遷移的HB(SW)

int main() {
  int g = 0;
  atomic_int x = 0;
  atomic_int y = 0;
  {{{ { g = 1;
        x.store(1, memory_order_release); }
  ||| { r0 = x.load(memory_order_consume).readsvalue(1);
        y.store(1, memory_order_release); }
  ||| { r1 = y.load(memory_order_acquire).readsvalue(1);
        r2 = g; }
  }}}
  return 0;
}
// 8 executions; 1 consistent, race free

rel-acq+rel-con関係/非遷移

int main() {
  int g = 0;
  atomic_int x = 0;
  atomic_int y = 0;
  {{{ { g = 1; /* data race */
        x.store(1, memory_order_release); }
  ||| { r0 = x.load(memory_order_acquire).readsvalue(1);
        y.store(1, memory_order_release); }
  ||| { r1 = y.load(memory_order_consume).readsvalue(1);
        r2 = g; /* data race */ }
  }}}
  return 0;
}
// 8 executions; 1 consistent, not race free

rel-con+同一スレッドrel-acq/Not DRF

int main() {
  int g = 0;
  atomic_int x = 0;
  atomic_int y = 0;
  {{{ { g = 1; /* data race */
        x.store(1, memory_order_release); }
  ||| { r0 = x.load(memory_order_consume).readsvalue(1);
        y.store(1, memory_order_release);
        /* rel-acq ops on same thread */
        r1 = y.load(memory_order_acquire).readsvalue(1);
        r2 = g; /* data race */ }
  }}}
  return 0;
}
// 8 executions; 1 consistent, not race free

release sequence-acq関係/DRF

int main() {
  int a = 0;
  atomic_int x = 0;
  {{{ { a = 42;
        x.store(1, memory_order_release);
        x.store(2, memory_order_relaxed); }
  ||| { r0 = x.load(memory_order_acquire).readsvalue(2);
        r1 = a; }
  }}}
  return 0;
}
// 12 executions; 1 consistent, race free

release sequence-acq関係/Not DRF

int main() {
  int a = 0;
  atomic_int x = 0;
  {{{ { a = 42; /* data race */
        x.store(1, memory_order_release); /* mo#1 */
        x.store(2, memory_order_relaxed); /* mo#3 */ }
  ||| { x.store(3, memory_order_relaxed); /* mo#2 */
        r0 = x.load(memory_order_acquire).readsvalue(2);
        r1 = a; /* data race */ }
  }}}
  return 0;
}
// 48 executions; 2 consistent, only 1 race free