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