vMVCC: Verified transaction library using multi-version concurrency control
vMVCC is a transaction library aimed at reducing the effort of writing
concurrent application code. It is implemented in Go and verified with
Perennial,
Iris, and Coq. This repository contains its
implementation. You can find its formal specification and proof
here.
For a high-level overview of its system architecture and proof, please refer to
our OSDI'23 paper.
Limitations
- Interface limited to
uint64
keys and string
values
- No durability
- No range query
Usage
See examples/hello.go
for a minimal example of using
vMVCC.
Import vMVCC
import "github.com/mit-pdos/vmvcc/vmvcc"
Creating a database and activating garbage collection
func MkDB() *DB
func (db *DB) ActivateGC()
Reading and writing the database
Define your transaction body with the following methods:
func (txn *Txn) Read(key uint64) (string, bool)
func (txn *Txn) Write(key uint64, val string)
func (txn *Txn) Delete(key uint64) bool
Executing transactions
Pick one of the approaches below to execute transactions.
Approach 1: db.Run
Pass your transaction body to db.Run
to run the transaction atomically:
func (db *DB) Run(body func(txn *Txn) bool) bool
It is safe to call db.Run
concurrently on multiple threads.
Approach 2: txn.Run
To reduce memory allocation for transaction objects, and to have more control
over the assignment of transaction sites, another way to run transactions is
with the following approach: (1) create a transaction object txn
with
db.NewTxn
, and (2) call txn.Run
to run the transaction atomically.
func (db *DB) NewTxn() *Txn
func (txn *Txn) Run(body func(txn *Txn) bool) bool
You can reuse txn
as many times as you want, and it is safe to call Run
concurrently with different transaction objects. However, it is NOT
safe to call Run
with the same transaction object concurrently.
Transactions with arguments
Both Run
methods (on Txn
and on DB
) expect a function that takes a single
transaction object; use function closures to
define your transaction with additional arguments. See
examples/xfer.go
for an example.
Reproducing the results in the OSDI'23 paper
All the scripts for reproducing the results in the paper can be found in
osdi23/scripts
.
Run all the experiments with ./osdi23/scripts/all.sh
. The results will be
generated in the CSV format under the ./exp
directory.