Project overview
The goal of this project is to build and formally verify practical and high-performance transactional database systems, based on the Perennial verification framework. Our OSDI ‘23 vMVCC paper reports on our first step toward the goal: verifying a high-performance transaction library.
vMVCC
vMVCC is a high-performance transaction library with a formal specification and a machine-checked proof of correctness. vMVCC addresses the core technical challenge faced by the transaction layer in a database—correctly and efficiently executing concurrent transactions.
vMVCC adopts multi-version concurrency control (MVCC), a popular technique used in many other research and commercial database systems. MVCC improves concurrency by retaining past versions for readers to read, while allowing writers to add new versions. Formally reasoning about MVCC requires advanced proof techniques, such as logical atomicity and prophecy variables.
Results
People
- Yun-Sheng Chang (PhD)
- Upamanyu Sharma (PhD)
- Prof. Ralf Jung (ETH Zürich)
- Prof. Joseph Tassarotti (New York University)
- Prof. M. Frans Kaashoek
- Prof. Nickolai Zeldovich