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.
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.
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