Parallel Snapshot Isolation (PSI)
A standard database / distributed transactional consistency model, given a declarative (acyclicity-axiom) semantics by Raad, Lahav & Vafeiadis together with a simple lock-based reference implementation built on top of the release-acquire (RA) fragment of the C/C++11 memory model and proved sound and complete against the declarative specification — the first treatment of PSI as an STM model over a weak-memory programming language. PSI weakens serializability, letting conflicting transactions without a write-write conflict commit in parallel; it permits the write-skew anomaly and the long-fork anomaly (the latter forbidden under Snapshot Isolation). The authors also give Robust PSI (RPSI), extending PSI to mixed transactional/non-transactional code with its own sound-and-complete RA implementation.
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 out-of-thin-air
Ordering relationships
- Strictly weaker than
- Snapshot Isolation (SI) — Raad, Lahav & Vafeiadis: PSI is a weakening of Snapshot Isolation — the 'long fork' anomaly (IRIW-with-transactions) is allowed under PSI but disallowed under SI (ESOP 2018, §1), while SI permits only the write-skew anomaly and otherwise coincides with serializability (VMCAI 2019). So SI admits strictly fewer transactional behaviours than PSI.
- Compiles correctly to
- Repaired C11 (RC11) — Raad, Lahav & Vafeiadis (ESOP 2018) give PSI a lock-based reference implementation built on the release-acquire (RA) fragment of the C/C++11 memory model, proved sound and complete against the declarative PSI specification (and likewise Robust PSI). The target is the RA fragment of RC11.
References
- Azalea Raad, Ori Lahav, Viktor Vafeiadis. On Parallel Snapshot Isolation and Release/Acquire Consistency. ESOP 2018, 2018. doi:10.1007/978-3-319-89884-1_33