Persistent Serialisability (PSER)

2019 · Raad, Wickerson, Vafeiadis · theoretical, formal · axiomatic formalism

A transactional persistency model giving the first formalisation of transactional semantics in the non-volatile-memory setting: it extends serialisability with an orthogonal persist-order axiom over durable transactions. Proven to compile correctly to PARMv8.

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.

Reasoning guarantees: yes Coherence
yes No undefined behaviour
yes No out-of-thin-air

Ordering relationships

Compiles correctly to: Persistent ARMv8 (PARMv8) — Raad, Wickerson & Vafeiadis (OOPSLA 2019) prove that PSER (persistent serialisability) compiles correctly to PARMv8.

References

Azalea Raad, John Wickerson, Viktor Vafeiadis. Weak Persistency Semantics from the Ground Up: Formalising the Persistency Semantics of ARMv8 and Transactional Models. PACMPL 3(OOPSLA), Article 135, 2019. doi:10.1145/3360561

Open PSER in the interactive map →