Snapshot Isolation (SI)
The snapshot-isolation transactional consistency model — the default in many databases — given simplified, timestamp-free semantics by Raad, Lahav & Vafeiadis as two lock-based multiple-readers-single-writer (MRSW) reference implementations (one eager/prescient, one lazy) built over the release-acquire (RA) fragment of C/C++11 and proved sound and complete against the declarative (acyclicity-axiom) SI specification. SI permits only the write-skew anomaly and otherwise coincides with serializability; it is strictly stronger than Parallel Snapshot Isolation, forbidding the long-fork anomaly PSI allows. The paper also introduces Robust SI (RSI) for mixed transactional/non-transactional code, again with sound-and-complete RA implementations.
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 stronger than
- Parallel Snapshot Isolation (PSI) — 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 (VMCAI 2019) give SI two timestamp-free lock-based (MRSW) reference implementations built on the release-acquire (RA) fragment of C/C++11, proved sound and complete against the declarative SI specification (and likewise Robust SI). The target is the RA fragment of RC11.
References
- Azalea Raad, Ori Lahav, Viktor Vafeiadis. On the Semantics of Snapshot Isolation. VMCAI 2019, 2019. doi:10.1007/978-3-030-11245-5_1