Institute of Information Science, Academia Sinica

Multi-version concurrency control (MVCC) is a widely used, sophisticated approach for handling concurrent transactions in a database system.  vMVCC is the first MVCC-based database that comes with a machine-checked proof of correctness, providing clients with a guarantee that it will correctly handle all transactions despite a sophisticated design and implementation that might otherwise be error-prone.  vMVCC is implemented in Go, as a single-node in-memory database, and uses several optimizations, such as RDTSC-based timestamps, to achieve high performance (30-71% 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 sophisticated proof techniques, such as prophecy variables and logical atomicity, owing to the fact that MVCC transactions can linearize at timestamps prior to transaction execution.