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.
Cat model
Expressible in cat author-extrapolated
Declarative persistency axioms over Armv8 executions (aarch64.cat plus a persist-order axiom in shape); no cat model exists for the persistency dimension. Cho et al. 2021
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