Verifying vMVCC, a high-performance transaction library using multi-version concurrency..
summary
vMVCC claims to be the first MVCC transaction library with a machine-checked proof and ships as about 800 lines of Go (open source). It implements in-memory MVCC with per-transaction RDTSC timestamps, version garbage collection, and reaches 25–96% of Silo’s throughput on YCSB/TPC-C; a non-versioning in-place variant shows versioning cost. The formal side uses a 42-line spec and ~11k lines of proof mechanized in Iris, relying on privacy variables and prophecy variables to handle linearization-at-timestamp and speculative commits.
AI-written summary · about
chapters (8)
- 0:00Verifying vMVCC
- 2:54vMVCC implementation
- 6:25Formal spec and benefits
- 7:06Verification with prophecy
- 9:14Proof and details
- 10:19Bugs caught verifying
- 10:39Performance vs state-of-the-art
- 12:43Related work and conclusion
related talks
01h 11mMVCC unmasked
45mTransactions and Concurrency Control Patterns
28mUnderstanding Transaction Isolation for App Developers
41mTransactions: myths, surprises and opportunities
14mMotor: Enabling Multi-Versioning for Distributed Transactions on Disaggregated Memory
48mLightning Talks
50mWe have multiple concurrent versions of this title trying to understand MVCC
50mExplaining the PG concurrency control mechanisms using rollercoasters