Reasoning about Weak Isolation Levels in Separation Logic
summary
Paper formalizes three weak isolation levels for key-value transactions and mechanizes them in Rocq on Iris, giving atomic-style separation-logic specs for read uncommitted, read committed, and snapshot isolation. It proves implication theorems (snapshot → read committed → read uncommitted) and verifies an executable multi-version concurrency control prototype (timestamped MVCC) against the snapshot spec. Artifacts and verified OCaml-to-logic transpiler are available, and the implementation satisfies the spec in the mechanized development.
AI-written summary · about
chapters (18)
- 0:00Transactional databases intro
- 1:48Why transactions matter
- 3:54Baseline guarantees
- 6:43Serializability isolation
- 7:50Snapshot isolation
- 8:54Banking example isolation
- 11:00Verifying weak isolation
- 12:24Separation logic with AnARIS
- 13:49Paper contributions
- 14:57Isolation levels in logic
- 16:25Snapshot isolation resources
- 18:54Start operation resources
- 19:35Read/write under snapshot
- 20:19Commit conflict checks
- 21:23Formal proof implications
- 22:46Verified DB implementation
- 23:50Contributions summary
- 24:31Q&A
related talks
16mDynamic Partial Order Reduction for Checking Correctness Against Transaction Isolation(…)
21mIsoPredict: Dynamic Predictive Analysis for Detecting Unserializable Behaviors in Weakly(…)
58mConcurrency in Postgres
52mTransactions: Myths, Surprises and Opportunities
29mPutting Rails in a corner: Understanding database isolation
47mBeing transactional in 2019 - what does this actually mean?
47mMaximizing Database Performance With Isolation Levels- 47mMaximizing Database Performance With Isolation Levels