View-based PArmv8 (PArmv8view)
The first operational persistency model for Armv8, part of Cho et al.'s view-based revamp of hardware persistency. It extends the Armv8view consistency model with persistency views over the store/persist history in the same uniform operational style as Px86view, differing in the ordering imposed by flushes and the absence of a strong-flush primitive. Proven equivalent (mechanised in Coq) to the axiomatic PArmv8axiom; 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
- Axiomatic PArmv8 (PArmv8axiom) — 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