Promising-ARM/RISC-V P-ARM/RV
A timestamp-based operational concurrency model for the ARMv8 and RISC-V instruction sets. It computes allowed behaviours incrementally from thread-local conditions, executing instructions in program order (bar early writes) without branch speculation, giving a substantially simpler operational presentation than prior ARM/RISC-V operational models. It reworks the timestamp/promise approach of the C/C++ Promising Semantics with a new uniform treatment of dependencies, but targets ISAs rather than C/C++, so it is a distinct model. Proven equivalent in Coq (for finite executions) to the axiomatic ARMv8 and RVWMO models.
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
- yes Load→Store
- Reasoning guarantees
- yes Coherence
- yes No undefined behaviour
- no In-order execution
- yes No out-of-thin-air
- Atomicity guarantees
- yes Multicopy atomic
Ordering relationships
- Equivalent to
- ARMv8 / AArch64 Memory Model — Pulte et al. (PLDI 2019), Appendix D, Theorem D.1: the operational Promising-ARM model is proven equivalent in Coq to the axiomatic ARMv8 model for finite executions.
- RISC-V Weak Memory Ordering (RVWMO) — Pulte et al. (PLDI 2019), Appendix D, Theorem D.2: the operational Promising-RISC-V model is proven equivalent in Coq to the axiomatic RVWMO model for finite executions.
References
- Christopher Pulte, Jean Pichon-Pharabod, Jeehoon Kang, Sung-Hwan Lee, Chung-Kil Hur. Promising-ARM/RISC-V: A Simpler and Faster Operational Concurrency Model. PLDI 2019, 2019. doi:10.1145/3314221.3314624
- 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