Persistent TSO (PTSO)

2018 · Raad, Vafeiadis · hardware, formal · axiomatic, operational formalism

Persistent-memory model layering buffered epoch persistency on top of the TSO / x86-TSO consistency model. It adds an orthogonal persist-order axiom (what survives a crash on non-volatile memory) rather than reordering reads/writes: the crash-free behaviour coincides with TSO, while persistency governs the order in which store-buffered writes reach NVM. 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: x86-TSO — Raad & Vafeiadis (OOPSLA 2018): PTSO layers epoch persistency on TSO; on the crash-free fragment its behaviour coincides with x86-TSO. fragment_restricted because the equivalence holds only crash-free — persistency adds an orthogonal persist-order dimension the consistency model does not see.

References

Azalea Raad, Viktor Vafeiadis. Persistence Semantics for Weak Memory: Integrating Epoch Persistency with the TSO Memory Model. PACMPL 2(OOPSLA), Article 137, 2018. doi:10.1145/3276507

Open PTSO in the interactive map →