Efficient Black-box Checking of Snapshot Isolation in Databases

TL;DR

PolySI is a new black-box tool that efficiently detects snapshot isolation violations in databases, providing clear counterexamples and scaling well to large workloads.

Contribution

It introduces PolySI, a novel black-box checker for snapshot isolation that uses generalized polygraphs and SMT solving to detect violations effectively.

Findings

Reproduces all 2477 known SI anomalies

Detects new SI violations in cloud databases

Outperforms existing black-box checkers

Abstract

Snapshot isolation (SI) is a prevalent weak isolation level that avoids the performance penalty imposed by serializability and simultaneously prevents various undesired data anomalies. Nevertheless, SI anomalies have recently been found in production cloud databases that claim to provide the SI guarantee. Given the complex and often unavailable internals of such databases, a black-box SI checker is highly desirable. In this paper we present PolySI, a novel black-box checker that efficiently checks SI and provides understandable counterexamples upon detecting violations. PolySI builds on a novel characterization of SI using generalized polygraphs (GPs), for which we establish its soundness and completeness. PolySI employs an SMT solver and also accelerates SMT solving by utilizing the compact constraint encoding of GPs and domain-specific optimizations for pruning constraints. As demonstrated by our extensive assessment, PolySI successfully reproduces all of 2477 known SI anomalies, detects novel SI violations in three production cloud databases, identifies their causes, outperforms the state-of-the-art black-box checkers under a wide range of workloads, and can scale up to large-sized workloads.