Persistent x86 (Px86)
First formalisation of the persistency semantics of the Intel-x86 architecture, layering a persist-order axiom (what survives a crash on non-volatile memory) on top of the x86 (x86-TSO) consistency model. Given both operationally and declaratively, with the two shown equivalent. The persist dimension is orthogonal to x86's store-load reordering; 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
- x86-TSO — Raad, Wickerson, Neiger & Vafeiadis (POPL 2020): Px86's crash-free behaviour coincides with x86-TSO. fragment_restricted because the equivalence holds only on the crash-free fragment; the persist-order axiom is orthogonal.
- Synchronous PTSO (PTSOsyn) — Khyzha & Lahav (POPL 2021): the synchronous-persist model PTSOsyn is proven equivalent, in terms of reachable states, to Raad et al.'s asynchronous-persist Px86 (POPL 2020). Full equivalence (crashes included), so not fragment_restricted; the caveat is that it is a state-based / reachable-state equivalence rather than a full trace equivalence.
- Axiomatic Px86 (Px86axiom) — 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.
- Persistent Ex86 (PEx86) — Raad, Maranget & Vafeiadis (POPL 2022): PEx86 is a conservative extension of Px86 (Px86sim) -- for programs using only regular stores on write-back memory (no non-temporal stores or non-wb memory types) their behaviours coincide. fragment_restricted because it holds only on that shared wb regular-store fragment; and even there PEx86 minorly diverges from Px86sim by dropping the flush/flushopt ordering constraint, following the updated Intel manual.
References
- Azalea Raad, John Wickerson, Gil Neiger, Viktor Vafeiadis. Persistency Semantics of the Intel-x86 Architecture. PACMPL 4(POPL), Article 11, 2020. doi:10.1145/3371079