{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T04:41:35Z","timestamp":1773895295979,"version":"3.50.1"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"5","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. VLDB Endow."],"published-print":{"date-parts":[[2025,1]]},"abstract":"<jats:p>\n            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\n            <jats:italic toggle=\"yes\">rigorous<\/jats:italic>\n            and\n            <jats:italic toggle=\"yes\">systematic<\/jats:italic>\n            framework with tool support for formally verifying a wide range of such guarantees for\n            <jats:italic toggle=\"yes\">all<\/jats:italic>\n            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.\n          <\/jats:p>","DOI":"10.14778\/3718057.3718065","type":"journal-article","created":{"date-parts":[[2025,8,27]],"date-time":"2025-08-27T18:11:49Z","timestamp":1756318309000},"page":"1362-1375","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["VerIso: Verifiable Isolation Guarantees for Database Transactions"],"prefix":"10.14778","volume":"18","author":[{"given":"Shabnam","family":"Ghasemirad","sequence":"first","affiliation":[{"name":"ETH Zurich, Switzerland"}]},{"given":"Si","family":"Liu","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}]},{"given":"Christoph","family":"Sprenger","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}]},{"given":"Luca","family":"Multazzu","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}]},{"given":"David","family":"Basin","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}]}],"member":"320","published-online":{"date-parts":[[2025,8,27]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_2_1_2_1","unstructured":"Atul Adya. 1999. Weak consistency: a generalized theory and optimistic implementations for distributed transactions. Ph.D. Dissertation. Massachusetts Institute of Technology Department of Electrical Engineering and Computer Science."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDCS.2016.98"},{"key":"e_1_2_1_4_1","volume-title":"azure-cosmos-tla. Retrieved","year":"2025","unstructured":"Azure. 2022. azure-cosmos-tla. Retrieved March 7, 2025 from https:\/\/github.com\/Azure\/azure-cosmos-tla"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2909870"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/223784.223785"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/356842.356846"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360591"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the 2021 USENIX Annual Technical Conference, USENIX ATC 2021, Irina Calciu and Geoff Kuenning (Eds.). USENIX Association, 923\u2013937","author":"Bravo Manuel","year":"2021","unstructured":"Manuel Bravo, Alexey Gotsman, Borja de R\u00e9gil, and Hengfeng Wei. 2021. UniStore: A fault-tolerant marriage of causal and strong consistency. In Proceedings of the 2021 USENIX Annual Technical Conference, USENIX ATC 2021, Irina Calciu and Geoff Kuenning (Eds.). USENIX Association, 923\u2013937. https:\/\/www.usenix.org\/conference\/atc21\/presentation\/bravo"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2015.568"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CONCUR.2015.58"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.14778\/3476311.3476379"},{"key":"e_1_2_1_13_1","volume-title":"All about Maude - a High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic","author":"Clavel Manuel","unstructured":"Manuel Clavel, Francisco Dur\u00e1n, Steven Eker, Patrick Lincoln, Narciso Mart\u00ed-Oliet, Jos\u00e9 Meseguer, and Carolyn Talcott. 2007. All about Maude - a High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic. Springer-Verlag, Berlin, Heidelberg."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491245"},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the ACM Symposium on Principles of Distributed Computing (PODC'17)","author":"Crooks Natacha","year":"2017","unstructured":"Natacha Crooks, Youer Pu, Lorenzo Alvisi, and Allen Clement. 2017. Seeing is Believing: A Client-Centric Specification of Database Isolation. In Proceedings of the ACM Symposium on Principles of Distributed Computing (PODC'17). ACM, 73\u201382."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.14778\/3397230.3397233"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.14778\/3236187.3236210"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00101"},{"key":"e_1_2_1_19_1","unstructured":"ElectricSQL. 2024. Retrieved March 7 2025 from https:\/\/electric-sql.com\/"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2503.06284"},{"key":"e_1_2_1_21_1","volume-title":"TACAS 2025, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2025 (Lecture Notes in Computer Science). Springer. To appear.","author":"Ghasemirad Shabnam","year":"2025","unstructured":"Shabnam Ghasemirad, Christoph Sprenger, Si Liu, Luca Multazzu, and David Basin. 2025. Pushing the Limit: Verified Performance-Optimal Causally-Consistent Database Transactions. In Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2025 (Lecture Notes in Computer Science). Springer. To appear."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.14778\/3685800.3685866"},{"key":"e_1_2_1_23_1","volume-title":"CockroachDB beta passes Jepsen testing. Retrieved","author":"Hsieh Diana","year":"2025","unstructured":"Diana Hsieh. 2017. CockroachDB beta passes Jepsen testing. Retrieved March 7, 2025 from https:\/\/www.cockroachlabs.com\/blog\/cockroachdb-beta-passes-jepsen-testing\/"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.14778\/3583140.3583145"},{"key":"e_1_2_1_25_1","unstructured":"Jepsen. 2024. Jepsen Analyses. Retrieved March 7 2025 from https:\/\/jepsen.io\/analyses"},{"key":"e_1_2_1_26_1","volume-title":"17th USENIX Symposium on Operating Systems Design and Implementation, OSDI","author":"Jiang Zu-Ming","year":"2023","unstructured":"Zu-Ming Jiang, Si Liu, Manuel Rigger, and Zhendong Su. 2023. Detecting Transactional Bugs in Database Engines via Graph-Based Oracle Construction. In 17th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2023, Roxana Geambasu and Ed Nightingale (Eds.). USENIX Association, 397\u2013417. https:\/\/www.usenix.org\/conference\/osdi23\/presentation\/jiang"},{"key":"e_1_2_1_27_1","unstructured":"Kyle Kingsbury. 2018. Dgraph 1.0.2. Retrieved March 7 2025 from https:\/\/jepsen.io\/analyses\/dgraph-1-0-2"},{"key":"e_1_2_1_28_1","unstructured":"Kyle Kingsbury. 2019. YugaByte DB 1.3.1. Retrieved March 7 2025 from https:\/\/jepsen.io\/analyses\/yugabyte-db-1.3.1"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.14778\/3430915.3430918"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837622"},{"key":"e_1_2_1_31_1","volume-title":"Remove SNAPSHOT ISOLATION mention from FAQ page #349. Retrieved","author":"Library Galera Cluster","year":"2025","unstructured":"Galera Cluster Library. 2023. Remove SNAPSHOT ISOLATION mention from FAQ page #349. Retrieved March 7, 2025 from https:\/\/github.com\/codership\/documentation\/commit\/cc8d6125f1767493eb61e2cc82f5a365ecee6e7a"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3494517"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689742"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3639264"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/S00165-019-00489-W"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17465-1_3"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the 10th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2013, Nick Feamster and Jeffrey C. Mogul (Eds.). USENIX Association, 313\u2013328","author":"Lloyd Wyatt","unstructured":"Wyatt Lloyd, Michael J. Freedman, Michael Kaminsky, and David G. Andersen. 2013. Stronger Semantics for Low-Latency Geo-Replicated Storage. In Proceedings of the 10th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2013, Nick Feamster and Jeffrey C. Mogul (Eds.). USENIX Association, 313\u2013328. https:\/\/www.usenix.org\/conference\/nsdi13\/technical-sessions\/presentation\/lloyd"},{"key":"e_1_2_1_39_1","volume-title":"The SNOW Theorem and Latency-Optimal Read-Only Transactions. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI","author":"Lu Haonan","year":"2016","unstructured":"Haonan Lu, Christopher Hodsdon, Khiem Ngo, Shuai Mu, and Wyatt Lloyd. 2016. The SNOW Theorem and Latency-Optimal Read-Only Transactions. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Kimberly Keeton and Timothy Roscoe (Eds.). USENIX Association, 135\u2013150. https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/lu"},{"key":"e_1_2_1_40_1","volume-title":"17th USENIX Symposium on Operating Systems Design and Implementation (OSDI 23)","author":"Lu Haonan","year":"2023","unstructured":"Haonan Lu, Shuai Mu, Siddhartha Sen, and Wyatt Lloyd. 2023. NCC: Natural Concurrency Control for Strictly Serializable Datastores by Avoiding the Timestamp-Inversion Pitfall. In 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI 23). USENIX Association, 305\u2013323."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1134"},{"key":"e_1_2_1_42_1","volume-title":"14th USENIX Symposium on Networked Systems Design and Implementation, NSDI","author":"Mehdi Syed Akbar","year":"2017","unstructured":"Syed Akbar Mehdi, Cody Littley, Natacha Crooks, Lorenzo Alvisi, Nathan Bronson, and Wyatt Lloyd. 2017. I Can't Believe It's Not Causal! Scalable Causal Consistency with No Slowdown Cascades. In 14th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2017, Aditya Akella and Jon Howell (Eds.). USENIX Association, 453\u2013468. https:\/\/www.usenix.org\/conference\/nsdi17\/technical-sessions\/presentation\/mehdi"},{"key":"e_1_2_1_43_1","volume-title":"Consistency levels in Azure Cosmos DB. Retrieved","year":"2025","unstructured":"Microsoft. 2024. Consistency levels in Azure Cosmos DB. Retrieved March 7, 2025 from https:\/\/learn.microsoft.com\/en-us\/azure\/cosmos-db\/consistency-levels"},{"key":"e_1_2_1_44_1","unstructured":"MongoDB. 2024. Retrieved March 7 2025 from https:\/\/www.mongodb.com\/"},{"key":"e_1_2_1_45_1","unstructured":"Neo4j. 2024. Retrieved March 7 2025 from https:\/\/neo4j.com\/"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10542-0"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/322154.322158"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043592"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2020.3026778"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428220"},{"key":"e_1_2_1_53_1","unstructured":"Informal Systems. 2024. Apalache. Retrieved March 7 2025 from https:\/\/apalache.informal.systems\/"},{"key":"e_1_2_1_54_1","volume-title":"Cobra: Making Transactional Key-Value Stores Verifiably Serializable. In 14th USENIX Symposium on Operating Systems Design and Implementation, OSDI","author":"Tan Cheng","year":"2020","unstructured":"Cheng Tan, Changgeng Zhao, Shuai Mu, and Michael Walfish. 2020. Cobra: Making Transactional Key-Value Stores Verifiably Serializable. In 14th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2020. USENIX Association, 63\u201380. https:\/\/www.usenix.org\/conference\/osdi20\/presentation\/tan"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815419"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2020.21"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815404"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3269981"},{"key":"e_1_2_1_59_1","unstructured":"Irene Zhang Naveen Kr. Sharma Michael Whittaker and Maxime Caron. 2019. TAPIR. Retrieved March 7 2025 from https:\/\/github.com\/UWSysLab\/tapir"}],"container-title":["Proceedings of the VLDB Endowment"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.14778\/3718057.3718065","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,27]],"date-time":"2025-08-27T18:13:29Z","timestamp":1756318409000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.14778\/3718057.3718065"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1]]},"references-count":59,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2025,1]]}},"alternative-id":["10.14778\/3718057.3718065"],"URL":"https:\/\/doi.org\/10.14778\/3718057.3718065","relation":{},"ISSN":["2150-8097"],"issn-type":[{"value":"2150-8097","type":"print"}],"subject":[],"published":{"date-parts":[[2025,1]]},"assertion":[{"value":"2025-08-27","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}