Axiomatic PArmv8 (PArmv8axiom)
Cho et al.'s declarative Armv8 persistency model, which simplifies and fixes documented flaws in Raad et al.'s PARMv8. Formally, they prove (Thm 6.1) that PArmv8axiom is equivalent to SPArmv8, a strengthening of PARMv8, and (Thm 6.2) that it is equivalent to the operational PArmv8view. This axiomatic model has been reviewed by Arm engineers; the crash-free behaviour coincides with Armv8.
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
- View-based PArmv8 (PArmv8view) — Cho, Lee, Raad & Kang (PLDI 2021), Theorem 6.2: a behaviour is allowed under PArmv8axiom iff it is allowed under the operational PArmv8view. Full equivalence (mechanised in Coq), covering the persistency dimension, hence not fragment_restricted.
References
- Kyeongmin Cho, Sung-Hwan Lee, Azalea Raad, Jeehoon Kang. Revamping Hardware Persistency Models: View-Based and Axiomatic Persistency Models for Intel-x86 and Armv8. PLDI 2021, 2021. doi:10.1145/3453483.3454027