Persistent Ex86 (PEx86)
Extends the Px86 (Px86sim) persistency model of Raad et al. to cover the full range of Intel-x86 memory types (uncacheable, write-combined, write-through, write-back) and non-temporal stores (MOVNT), together with their subtle interactions, validated by extensive testing on real Intel-x86 hardware. PEx86 is a conservative extension of Px86sim: for programs restricted to regular stores on write-back memory it coincides with Px86, differing only in a minor divergence over flush/flushopt ordering that PEx86 drops to follow the updated Intel manual. Given both operationally and declaratively.
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
- Persistent x86 (Px86) — 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, Luc Maranget, Viktor Vafeiadis. Extending Intel-x86 Consistency and Persistency: Formalising the Semantics of Intel-x86 Memory Types and Non-temporal Stores. PACMPL 6(POPL), Article 22, 2022. doi:10.1145/3498683