Axiomatic Px86 (Px86axiom)
Cho et al.'s declarative Intel-x86 persistency model, which simplifies and fixes documented flaws in Raad et al.'s Px86. Formally, they prove (Thm 4.3) that Px86axiom is equivalent to SPx86, a strengthening of Px86 that executes clflush synchronously, and (Thm 5.3) that it is equivalent to the operational Px86view. 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
- View-based Px86 (Px86view) — 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.
- Persistent x86 (Px86) — Equivalent modulo Cho's fix. Cho, Lee, Raad & Kang (PLDI 2021), Theorem 4.3, prove Px86axiom equivalent to SPx86 -- a *strengthened* Px86 whose clflush executes synchronously -- which repairs documented flaws in Raad et al.'s original Px86. So this is an equivalence to the fixed model, not literally the original Px86; fragment_restricted because the two coincide only on the fragment where those flaws do not manifest.
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