View-based Px86 (Px86view)
The first operational, view-based persistency model for Intel-x86, part of Cho et al.'s revamp of hardware persistency. Each thread tracks views over the store/persist history in a uniform operational style, extending the x86view consistency model with persistency. Proven equivalent (mechanised in Coq) to the axiomatic Px86axiom, and thereby to Raad et al.'s Px86 modulo the flaws Cho et al. repair. The crash-free behaviour coincides with x86-TSO.
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
- no Store→Store
- no Load→Load
- no Load→Store
- Reasoning guarantees
- yes Coherence
- yes No undefined behaviour
- yes In-order execution
- yes No out-of-thin-air
- Atomicity guarantees
- yes Multicopy atomic
Ordering relationships
- Equivalent to
- Axiomatic Px86 (Px86axiom) — Cho, Lee, Raad & Kang (PLDI 2021), Theorem 5.3: a behaviour is allowed under Px86axiom iff it is allowed under the operational Px86view. 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