Ou–Demsky Load-Store-Ordering Criterion OD-LSO
An execution criterion that forbids out-of-thin-air (OOTA) results by preserving load→store ordering, requiring the union of sequence-before and reads-from to be acyclic. Targeted at C/C++-like memory models in which racing operations are explicitly labelled atomic, so it constrains only relaxed atomics; the authors implement it in the LLVM AArch64 backend and report no average overhead (6.3% worst case) on concurrent data-structure benchmarks. A strictly stronger guarantee than the paper's dependency-preserving criterion.
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
- no Load→Store
- Reasoning guarantees
- yes Coherence
- yes No out-of-thin-air
Ordering relationships
- Strictly weaker than
- Sequential Consistency (SC) — Ou & Demsky 2018, §6: 'the constraints we impose in general are much weaker than the sequential consistency memory model.' The load-store-ordering criterion permits relaxed-atomics reorderings SC forbids while ruling out OOTA.
- Strictly stronger than
- Ou–Demsky Dependency-Preserving Criterion (OD-Dep) — 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.
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