Promising Semantics 1.0 PS
An operational model for relaxed memory based on the notion of thread-local 'promises': a thread may promise a future write, provided it can certify the promise by a thread-local execution under every possible future memory. Eliminates thin-air values, supports DRF guarantees and validates the standard thread-local optimisations, but not global ones such as register promotion or value-range analysis, and its relaxed RMWs need an extra fence on ARMv8. Has no SC accesses. Superseded by PS 2.0, which redesigns certification.
Cat model
Not expressible in cat cited
A promise is legal only if the promising thread can certify it by a future thread-local execution, so whether one execution is allowed depends on other executions — not statable as a per-execution cat predicate. IMM was introduced precisely to give Promising a declarative over-approximation. Podkopaev et al. 2019
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.
- Compilation optimal mapping to
- yes x86
- yes POWER
- yes Armv7
- no Armv8 Lee et al. 2020
- 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
- no Register promotion Lee et al. 2020
- no Thread inlining
- no Value range Lee et al. 2020
- 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
- Compiles correctly to
- Intermediate Memory Model (IMM) — Podkopaev, Lahav & Vafeiadis (POPL 2019) prove in Coq that compilation from the Promising Semantics to IMM is correct, and from there to x86-TSO, POWER and ARMv8. On ARMv8, PS 1.0's relaxed RMWs need an extra ld fence, because the intended mapping is unsound (the FADD load-buffering, Chakraborty & Vafeiadis 2019 Fig. 6). PS 2.0 removes that fence.
- Incomparable with
- C11/C++11 Memory Model — PS 1.0 is an alternative to C11 at a similar level, not a direct subset or superset: C11 allows out-of-thin-air load buffering, which PS forbids by certification. PS 2.0 has no edge to C11 yet.
- 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.'
- Weakestmo (Event-Structure Model) (WMO) — Chakraborty & Vafeiadis (POPL 2019) §4.3 state that Weakestmo and PS (1.0, the 2017 model they compare against) are incomparable, with a witness each way: Coh-CYC (PS allows, Weakestmo forbids) and FADD (Weakestmo allows, PS forbids). Both are semantic-dependency-preserving models that forbid out-of-thin-air and give external DRF. Weakestmo is built on event structures rather than promises and certification, and unlike PS it supports SC accesses. PS 2.0 added reservations to fix the RMW mapping problem that FADD exposes, so it is not established that the FADD direction still holds for PS 2.0, and PS 2.0 has no edge to Weakestmo.
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.3386010
- Anton Podkopaev, Ori Lahav, Viktor Vafeiadis. Bridging the Gap between Programming Languages and Hardware Weak Memory Models. POPL 2019, 2019. doi:10.1145/3290382