Persistent Sequential Consistency (PSC)

2021 · Khyzha, Lahav · theoretical, formal · axiomatic, operational formalism

A simpler and stronger sequentially-consistent persistency model introduced alongside PTSOsyn: it layers an epoch-persistency dimension over SC rather than TSO, so the crash-free behaviour coincides with sequential consistency. Khyzha & Lahav develop a sound mapping from PSC down to x86 and establish a data-race-freedom guarantee giving programmers a safe programming discipline for persistent memory.

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: no 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

Compiles correctly to: x86-TSO — Khyzha & Lahav (POPL 2021) develop a sound mapping from the stronger SC-based persistency model PSC down to x86; the mapping targets the x86-TSO consistency model.

References

Artem Khyzha, Ori Lahav. Taming x86-TSO Persistency. PACMPL 5(POPL), Article 47, 2021. doi:10.1145/3434328

Open PSC in the interactive map →