Jian Zhang,
Ye Ji,
Shuai Mu,
and
Cheng Tan
EuroSys 2023,
May 8th-12th 2023, ROME, Italy
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 SI checking 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 15x in the number of transactions being checked.