Promising Semantics 2.0 PS 2.0
A redesign of the Promising Semantics' certification: promises are certified against a single 'capped' future memory rather than every future memory, and threads may reserve timestamp space for later RMWs. Keeps every PS 1.0 result (thread-local optimisations, hardware mappings, DRF theorems) and additionally validates global optimisations, namely register promotion and transformations based on value-range analysis. It also removes the extra fence that PS 1.0's relaxed RMWs needed on ARMv8. Compilation to x86-TSO, POWER, ARMv7, ARMv8 and RISC-V goes through IMM and is proved in Coq. Like PS 1.0 it has no SC accesses.
Cat model
Not expressible in cat cited
Certification still quantifies over a thread-local future execution (now against the capped memory), so whether one execution is allowed depends on other executions — not statable as a per-execution cat predicate. Its compilation proof goes through IMM, the declarative model that stands in for it. Lee et al. 2020
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
- Compiles correctly to
- Intermediate Memory Model (IMM) — Lee et al. (PLDI 2020), Theorem 6.9, mechanised in Coq: Beh_PS2.0(P) ⊇ Beh_IMM(P), so the mappings already proved correct from IMM (x86-TSO, POWER, ARMv7, ARMv8, RISC-V) are correct from PS 2.0, without PS 1.0's extra fence after RMWs. The mechanised proof needs a control dependency from the read part of each RMW, which relaxed fetch-and-adds must fake on ARMv8 (§6.5).
References
- 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
- 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