We present a mathematically rigorous, systematic approach for the verification of database isolation guarantees, which (i) supports a spectrum of seven isolation levels, (ii) uncovers a fundamental dichotomy among isolation levels: stronger levels can be verified via refinement alone, whereas weaker levels additionally require reduction, and (iii) provides a hierarchy of abstract models that substantially simplifies proofs by factoring out their most labor-intensive parts. In particular, we eliminate the need for per-protocol reduction proofs for the weaker class of isolation levels by performing a once-and-for-all reduction at a high level of abstraction in our hierarchy. To achieve this, we develop and apply a generic theory of reduction, which is also of more general interest. Overall, our approach minimizes the user’s proof effort to a single, simpler refinement of the most concrete model in our hierarchy. All our results are formalized in Isabelle/HOL.
@article{ghasemirad2026reduce,title={Reduce Once, Verify Many: Verifying Isolation Guarantees via Hierarchical Abstractions},author={Ghasemirad, Shabnam and Sprenger, Christoph and Liu, Si and Basin, David},booktitle={1st Symposium on Consistency Checking Principles (SCCP 2026), co-located with VLDB 2026},primaryclass={cs.PL},journal={arXiv preprint arXiv:2608.07793},year={2026},note={Accepted for presentation at SCCP 2026, co-located with VLDB 2026; non-archival},url={https://doi.org/10.48550/arXiv.2608.07793}}
2025
TACAS 2025
Pushing the Limit: Verified Performance-Optimal Causally-Consistent Database Transactions
Shabnam Ghasemirad, Christoph Sprenger, Si Liu, Luca Multazzu, and David A. Basin
In Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings, Part III, 2025
Modern web services crucially rely on high-performance distributed databases, where concurrent transactions are isolated from each other using concurrency control protocols. Relaxed isolation levels, which permit more complex concurrent behaviors than strong levels like serializability, are used in practice for higher performance and availability. In this paper, we present Eiger-PORT+, a concurrency control protocol that achieves a strong form of causal consistency, called TCCv (Transactional Causal Consistency with convergence). We show that Eiger-PORT+ also provides performance-optimal read transactions in the presence of transactional writes, thus refuting an open conjecture that this is impossible for TCCv. We also deductively verify that Eiger-PORT+ satisfies this isolation level by refining an abstract model of transactions. This yields the first deductive verification of a complex concurrency control protocol. Furthermore, we conduct a performance evaluation showing Eiger-PORT+ ’s superior performance over the state-of-the-art.
@inproceedings{DBLP:conf/tacas/GhasemiradSLMB25,author={Ghasemirad, Shabnam and Sprenger, Christoph and Liu, Si and Multazzu, Luca and Basin, David A.},editor={Gurfinkel, Arie and Heule, Marijn},title={Pushing the Limit: Verified Performance-Optimal Causally-Consistent
Database Transactions},booktitle={Tools and Algorithms for the Construction and Analysis of Systems
- 31st International Conference, {TACAS} 2025, Held as Part of the
International Joint Conferences on Theory and Practice of Software,
{ETAPS} 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings, Part
{III}},series={Lecture Notes in Computer Science},volume={15698},pages={43--62},publisher={Springer},year={2025},url={https://doi.org/10.1007/978-3-031-90660-2\_3},}
VLDB 2025
VerIso: Verifiable Isolation Guarantees for Database Transactions
Shabnam Ghasemirad, Si Liu, Christoph Sprenger, Luca Multazzu, and David A. Basin
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.
@article{DBLP:journals/corr/abs-2503-06284,author={Ghasemirad, Shabnam and Liu, Si and Sprenger, Christoph and Multazzu, Luca and Basin, David A.},title={{VerIso}: Verifiable Isolation Guarantees for Database Transactions},journal={Proc. {VLDB} Endow.},keywords={distributed database systems, transaction processing, consistency models},volume={18},year={2025},url={https://vldb.org/pvldb/volumes/18/paper/VerIso%3A%20Verifiable%20Isolation%20Guarantees%20for%20Database%20Transactions},}
2022
CoRR 2022
Efficient and Sound Differentiable Programming in a Functional Array-Processing Language
Amir Shaikhha, Mathieu Huot, Shabnam Ghasemirad, Andrew W. Fitzgibbon, Simon Peyton Jones, and Dimitrios Vytiniotis
@article{DBLP:journals/corr/abs-2212-10307,author={Shaikhha, Amir and Huot, Mathieu and Ghasemirad, Shabnam and Fitzgibbon, Andrew W. and Jones, Simon Peyton and Vytiniotis, Dimitrios},title={Efficient and Sound Differentiable Programming in a Functional Array-Processing
Language},journal={CoRR},volume={abs/2212.10307},year={2022},url={https://doi.org/10.48550/arXiv.2212.10307}}