Viper: A Fast Snapshot Isolation Checker

Snapshot isolation (SI) is supported by most commercial databases and is widely used by applications. However, checking SI today-given a set of transactions, checking if they obey SI-is either slow or gives up soundness.

We present viper, an SI checker that is sound, complete, and fast. Viper checks black-box databases and hence is transparent to both users and databases. To be fast, viper introduces BC-polygraphs, a new representation of transaction dependencies. A BC-polygraph is acyclic iff transactions are SI, a theorem that we prove. Viper also introduces heuristic pruning, an optimization to accelerate checking SI by leveraging common knowledge of real-world database implementations. Besides vanilla SI, viper supports major SI variants including Strong SI, Generalized SI, and Strong Session SI. Our experiments show that given the same time budget, viper improves over baselines by 15× in the workload sizes being checked.