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.

翻译：数十年来，在精心设计且经过广泛测试的生产数据库中，隔离性缺陷（尤其源于设计层面的问题）屡见不鲜。与此同时，多种用于建模数据库事务并推理其隔离性保证的框架相继被提出。然而，目前尚缺乏一个数学上严谨且系统化的框架，并辅以工具支持，以形式化验证所有可能系统行为下的广泛隔离性保证。我们提出了首个此类框架——VerIso，该框架在定理证明器 Isabelle/HOL 中开发。为展示其在验证中的应用，我们建模了严格两阶段锁定并发控制协议，并验证了其提供的严格可串行化隔离保证。此外，我们还展示了 VerIso 如何在协议设计阶段帮助识别隔离性缺陷。我们通过尝试证明 TAPIR 协议所声称的严格可串行化失败，为其推导出新的反例。具体而言，我们证明了该协议违反了一个弱得多的隔离级别，即原子可见性。