Fast Verification of Strong Database Isolation (Extended Version)

TL;DR

VeriStrong introduces hyper-polygraphs to model both certain and uncertain transactional dependencies under black-box observation, enabling sound and complete verification of Serializability and Snapshot Isolation. The core advance is tailoring SMT solving to database workloads, with preprocessing for small-width cycles and an order-guided polarity strategy, yielding substantial speedups over prior verifiers and scalability to large histories. Empirical results show VeriStrong outperforms state-of-the-art tools on supported workloads and remains effective on general workloads with duplicate writes, including real-world bugs in MariaDB/MySQL. The approach combines rigorous formal characterization with practical engineering to deliver fast, accurate isolation verification for deployed databases and complex workloads.

Abstract

Strong isolation guarantees, such as serializability and snapshot isolation, are essential for maintaining data consistency and integrity in modern databases. Verifying whether a database upholds its claimed guarantees is increasingly critical, as these guarantees form a contract between the vendor and its users. However, this task is challenging, particularly in black-box settings, where only observable system behavior is available and often involves uncertain dependencies between transactions. In this paper, we present VeriStrong, a fast verifier for strong database isolation. At its core is a novel formalism called hyper-polygraphs, which compactly captures both certain and uncertain transactional dependencies in database executions. Leveraging this formalism, we develop sound and complete encodings for verifying both serializability and snapshot isolation. To achieve high efficiency, VeriStrong tailors SMT solving to the characteristics of database workloads, in contrast to prior general-purpose approaches. Our extensive evaluation across diverse benchmarks shows that VeriStrong not only significantly outperforms state-of-the-art verifiers on the workloads they support, but also scales to large, general workloads beyond their reach, while maintaining high accuracy in detecting isolation anomalies.

Figures (18)

• Figure 1: Workflow for verifying isolation guarantees in deployed databases. Steps II and III are specific to SMT-based approaches (see also Sections \ref{['section:baseline']} and \ref{['sec:alg']}).
• Figure 2: Capturing Serializability via dependency graphs. Solid arrows denote known dependencies, whereas dashed arrows indicate uncertain ones.
• Figure 3: A general history $\mathcal{H}$, along with its hyper-polygraph $\mathcal{G}$ and two compatible graphs.
• Figure 4: An example solving process for $\mathcal{H}$ in Figure \ref{['fig:rw-checking']}.
• Figure 5: Cycle width distribution across conflicts.

Theorems & Definitions (13)

• definition 1
• definition 2
• definition 3
• theorem 1
• definition 4
• definition 5
• definition 6
• theorem 2
• definition 7
• theorem 3