VerIso: Verifiable Isolation Guarantees for Database Transactions
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866912265748348928 |
|---|---|
| author | Ghasemirad, Shabnam Liu, Si Sprenger, Christoph Multazzu, Luca Basin, David |
| author_facet | Ghasemirad, Shabnam Liu, Si Sprenger, Christoph Multazzu, Luca Basin, David |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_06284 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | VerIso: Verifiable Isolation Guarantees for Database Transactions Ghasemirad, Shabnam Liu, Si Sprenger, Christoph Multazzu, Luca Basin, David Databases Distributed, Parallel, and Cluster Computing Logic in Computer Science 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. |
| title | VerIso: Verifiable Isolation Guarantees for Database Transactions |
| topic | Databases Distributed, Parallel, and Cluster Computing Logic in Computer Science |
| url | https://arxiv.org/abs/2503.06284 |