Verifying vMVCC, a high-performance transaction library using multi-version concurrency control


Yun-Sheng Chang, MIT CSAIL; Ralf Jung, ETH Zurich; Upamanyu Sharma, MIT CSAIL; Joseph Tassarotti, New York University; M. Frans Kaashoek and Nickolai Zeldovich, MIT CSAIL


Multi-version concurrency control (MVCC) is a widely used, sophisticated approach for handling concurrent transactions. vMVCC is the first MVCC-based transaction library that comes with a machine-checked proof of correctness, providing clients with a guarantee that it will correctly handle all transactions despite a complicated design and implementation that might otherwise be error-prone. vMVCC is implemented in Go, stores data in memory, and uses several optimizations, such as RDTSC-based timestamps, to achieve high performance (25–96% the throughput of Silo, a state-of-the-art in-memory database, for YCSB and TPC-C workloads). Formally specifying and verifying vMVCC required adopting advanced proof techniques, such as logical atomicity and prophecy variables, owing to the fact that MVCC transactions can linearize at timestamp generation prior to transaction execution.

OSDI '23 Open Access Sponsored by
King Abdullah University of Science and Technology (KAUST)

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

@inproceedings {288544,
author = {Yun-Sheng Chang and Ralf Jung and Upamanyu Sharma and Joseph Tassarotti and M. Frans Kaashoek and Nickolai Zeldovich},
title = {Verifying {vMVCC}, a high-performance transaction library using multi-version concurrency control},
booktitle = {17th USENIX Symposium on Operating Systems Design and Implementation (OSDI 23)},
year = {2023},
isbn = {978-1-939133-34-2},
address = {Boston, MA},
pages = {871--886},
url = {},
publisher = {USENIX Association},
month = jul

Presentation Video