Promising Semantics PS
An operational model for relaxed memory based on the notion of thread-local 'promises': a thread may promise a future write and later fulfil it. Eliminates thin-air values, supports DRF-SC, and can express optimisation-friendly behaviour. Extended to PS 2.0 for mixed-size and non-atomic accesses.
Properties
Property vector survey-sourced — from Tables 1–2 of the Moiseenko et al. survey, except cells that cite a specific source.
- Compilation optimal mapping to
- yes x86
- yes POWER
- yes Armv7
- yes Armv8
- Reordering sound
- yes Store→Load
- yes Store→Store
- yes Load→Load
- yes Load→Store
- Elimination sound
- yes Store/Load
- yes Store/Store
- yes Load/Load
- yes Load/Store
- Other local transformations
- yes Irrelevant load elim.
- yes Speculative load intro.
- yes Roach motel
- yes Strengthening
- yes Trace preserving
- yes Common subexpr. elim.
- Global transformations
- yes Register promotion
- no Thread inlining
- yes Value range
- Reasoning guarantees
- yes External DRF
- yes Coherence
- yes No undefined behaviour
- no In-order execution
- yes No out-of-thin-air
- Atomicity guarantees
- no Multicopy atomic
Ordering relationships
- Incomparable with
- C11/C++11 Memory Model — Promising Semantics is an alternative to C11 at a similar level, not a direct subset/superset.
- Weakestmo (Event-Structure Model) (WMO) — Both are semantic-dependency-preserving models that forbid out-of-thin-air, admit the optimal compilation mappings, and give external DRF. Weakestmo is built on event structures (vs Promising's promises/certification) and, unlike the Promising semantics, supports sequentially consistent accesses; neither is a subset of the other.
- Concurrency Semantics for Relaxed Atomics (CSRA) — Both are semantic-dependency-preserving models avoiding thin-air; CSRA's compilation to x86 and POWER is sound, but unlike Promising its mappings to ARMv7/ARMv8 were later shown non-optimal. Neither contains the other.
- Pomsets with Predicate Transformers (The Leaky Semicolon) (PwT) — Leaky Semicolon §9: 'PwT-mca is incomparable to both RC11 ... and the promising semantics [Kang et al. 2017] ... PwT-mca has a weaker notion of coherence than the promising semantics.'
References
- Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer. A Promising Semantics for Relaxed-Memory Concurrency. POPL 2017, 2017. doi:10.1145/3009837.3009850
- Sung-Hwan Lee, Minki Cho, Anton Podkopaev, Soham Chakraborty, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis. Promising 2.0: Global Optimizations in Relaxed-Memory Concurrency. PLDI 2020, 2020. doi:10.1145/3385412.3386000