Persistent ARMv8 (PARMv8)
First formalisation of the persistency semantics of the ARMv8 architecture, layering a persist-order axiom (what survives a crash on non-volatile memory) on top of the ARMv8 consistency model. The persist dimension is orthogonal to ARMv8's read/write reordering; 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
- ARMv8 / AArch64 Memory Model — Raad, Wickerson & Vafeiadis (OOPSLA 2019): PARMv8's crash-free behaviour coincides with ARMv8. fragment_restricted because the equivalence holds only on the crash-free fragment; the persist-order axiom is orthogonal.
- Compilation target of
- Persistent Serialisability (PSER) — Raad, Wickerson & Vafeiadis (OOPSLA 2019) prove that PSER (persistent serialisability) compiles correctly to PARMv8.
References
- Azalea Raad, John Wickerson, Viktor Vafeiadis. Weak Persistency Semantics from the Ground Up: Formalising the Persistency Semantics of ARMv8 and Transactional Models. PACMPL 3(OOPSLA), Article 135, 2019. doi:10.1145/3360561