Synchronous PTSO (PTSOsyn)
An operational x86-TSO persistency model with synchronous explicit persist operations and per-cache-line persistence buffers, developed as a developer-friendly reformulation of Raad et al.'s Px86, whose persists are asynchronous. Khyzha & Lahav prove PTSOsyn equivalent, in terms of reachable states, to Px86, so its crash-free consistency coincides with x86-TSO while persistency is governed by synchronous per-line persists that are closer to programmers' intuition.
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) — 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.
References
- Artem Khyzha, Ori Lahav. Taming x86-TSO Persistency. PACMPL 5(POPL), Article 47, 2021. doi:10.1145/3434328