Ou–Demsky Dependency-Preserving Criterion OD-Dep
An execution criterion that forbids out-of-thin-air (OOTA) results by preserving a syntactic notion of dependency, requiring the union of (syntactic) dependency and reads-from to be acyclic. A strictly weaker guarantee than load-store ordering, targeted at Java-like languages in which every memory access can contribute to OOTA. Implemented in the LLVM compiler; the authors measure a 3.1% average (17.6% worst-case) overhead on SPEC CPU2006 for a prototype dependency-preserving compiler.
Properties
Property vector author-extrapolated — set only where the model’s definition pins the cell down (unknown cells are omitted); cells citing a specific source are marked.
- Reordering sound
- yes Store→Load
- yes Store→Store
- yes Load→Load
- Reasoning guarantees
- yes Coherence
- yes No out-of-thin-air
Ordering relationships
- Strictly weaker than
- Ou–Demsky Load-Store-Ordering Criterion (OD-LSO) — Ou & Demsky 2018, §1.3.2: preserving syntactic dependency (dependency ∪ reads-from acyclic) is explicitly 'a strictly weaker guarantee than the previous approach' of forbidding load-store reordering (sequence-before ∪ reads-from acyclic); dependency ⊆ sequence-before, so LSO-permitted executions are a subset of dependency-permitted ones.
- Strictly stronger than
- C11/C++11 Memory Model — Ou & Demsky 2018, §6: both approaches 'explore stronger memory models than the existing C/C++ memory model' — they forbid the OOTA/thin-air executions C11 permits while retaining ordinary relaxed-atomics reordering.
References
- Peizhao Ou, Brian Demsky. Towards Understanding the Costs of Avoiding Out-of-Thin-Air Results. Proc. ACM Program. Lang. 2 (OOPSLA), Article 136, 2018. doi:10.1145/3276506
- Hans-J. Boehm, Brian Demsky. Outlawing Ghosts: Avoiding Out-of-Thin-Air Results. MSPC 2014 (Workshop on Memory Systems Performance and Correctness), 2014. doi:10.1145/2618128.2618134