Fast Verification of Strong Database Isolation (Extended Version)

TL;DR

VeriStrong is a novel, efficient verifier for strong database isolation guarantees that uses hyper-polygraphs to accurately and quickly verify serializability and snapshot isolation in various workloads, including black-box scenarios.

Contribution

The paper introduces hyper-polygraphs and tailored SMT encodings, enabling fast, sound, and complete verification of database isolation guarantees in black-box settings.

Findings

VeriStrong outperforms existing verifiers on diverse benchmarks.

It scales to large, complex workloads beyond prior tools.

Maintains high accuracy in detecting isolation anomalies.

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.