VerIso: Verifiable Isolation Guarantees for Database Transactions
Shabnam Ghasemirad, Si Liu, Christoph Sprenger, Luca Multazzu, David Basin
TL;DR
VerIso presents a mechanized, Isabelle/HOL-based framework for rigorously verifying that database transaction protocols satisfy chosen isolation guarantees. By formalizing an abstract transaction model parameterized by isolation level and refining concrete protocols as LTSs, the approach proves correctness for arbitrary numbers of processes and transactions and supports automation through a large lemma library. The paper demonstrates the framework on Strict Two-Phase Locking (S2PL) to verify SSER, and uses it to uncover TAPIR’s atomic-visibility violations via counterexamples, illustrating both verification and falsification capabilities. This work offers a scalable, tool-supported pathway to design-stage correctness for concurrency-control protocols with broad practical impact for reliable database systems.
Abstract
Isolation bugs, stemming especially from design-level defects, have been repeatedly found in carefully designed and extensively tested production databases over decades. In parallel, various frameworks for modeling database transactions and reasoning about their isolation guarantees have been developed. What is missing however is a mathematically rigorous and systematic framework with tool support for formally verifying a wide range of such guarantees for all possible system behaviors. We present the first such framework, VerIso, developed within the theorem prover Isabelle/HOL. To showcase its use in verification, we model the strict two-phase locking concurrency control protocol and verify that it provides strict serializability isolation guarantee. Moreover, we show how VerIso helps identify isolation bugs during protocol design. We derive new counterexamples for the TAPIR protocol from failed attempts to prove its claimed strict serializability. In particular, we show that it violates a much weaker isolation level, namely, atomic visibility.