{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:06:50Z","timestamp":1784200010232,"version":"3.55.0"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>\n                    <jats:italic toggle=\"yes\">Database isolation<\/jats:italic>\n                    is a formal contract concerning the level of data consistency that a database provides to its clients. In order to achieve low latency, high throughput, and partition tolerance, modern databases forgo strong transaction isolation for\n                    <jats:italic toggle=\"yes\">weak isolation<\/jats:italic>\n                    guarantees. However, several production databases have been found to suffer from\n                    <jats:italic toggle=\"yes\">isolation bugs<\/jats:italic>\n                    , breaking their data-consistency contract.\n                    <jats:italic toggle=\"yes\">Black-box testing<\/jats:italic>\n                    is a prominent technique for detecting isolation bugs, by checking whether histories of database transactions adhere to a prescribed isolation level.\n                  <\/jats:p>\n                  <jats:p>\n                    In order to test databases on realistic workloads of large size, isolation testers must be as efficient as possible, a requirement that has initiated a study of the complexity of isolation testing. Although testing strong isolation has been known to be NP-complete, weak isolation levels were recently shown to be testable in polynomial time, which has propelled the scalability of testing tools. However, existing testers have a large polynomial complexity, restricting testing to workloads of only moderate size, which is not typical of large-scale databases.\n                    <jats:italic toggle=\"yes\">How efficiently can we provably test weak database isolation?<\/jats:italic>\n                  <\/jats:p>\n                  <jats:p>\n                    In this work, we develop AWDIT,\n                    <jats:italic toggle=\"yes\">a highly-efficient and provably optimal tester for weak database isolation<\/jats:italic>\n                    . Given a history\n                    <jats:italic toggle=\"yes\">H<\/jats:italic>\n                    of size\n                    <jats:italic toggle=\"yes\">n<\/jats:italic>\n                    and\n                    <jats:italic toggle=\"yes\">k<\/jats:italic>\n                    sessions, AWDIT tests whether\n                    <jats:italic toggle=\"yes\">H<\/jats:italic>\n                    satisfies the most common weak isolation levels of Read Committed (RC), Read Atomic (RA), and Causal Consistency (CC) in time\n                    <jats:italic toggle=\"yes\">O<\/jats:italic>\n                    (\n                    <jats:italic toggle=\"yes\">n<\/jats:italic>\n                    <jats:sup>3\/2<\/jats:sup>\n                    ),\n                    <jats:italic toggle=\"yes\">O<\/jats:italic>\n                    (\n                    <jats:italic toggle=\"yes\">n<\/jats:italic>\n                    <jats:sup>3\/2<\/jats:sup>\n                    ), and\n                    <jats:italic toggle=\"yes\">O<\/jats:italic>\n                    (\n                    <jats:italic toggle=\"yes\">n \u00b7 k<\/jats:italic>\n                    ), respectively, improving significantly over the state of the art. Moreover, we prove that AWDIT is essentially\n                    <jats:italic toggle=\"yes\">optimal<\/jats:italic>\n                    , in the sense that there is a lower bound of\n                    <jats:italic toggle=\"yes\">n<\/jats:italic>\n                    <jats:sup>3\/2<\/jats:sup>\n                    , based on the combinatorial BMM hypothesis, for\n                    <jats:italic toggle=\"yes\">any<\/jats:italic>\n                    weak isolation level between RC and CC. Our experiments show that AWDIT is significantly faster than existing, highly optimized testers; e.g., for the \u223c20\ufe6a largest histories, AWDIT obtains an average speedup of 245\u00d7, 193\u00d7, and 62\u00d7 for RC, RA, and CC, respectively, over the best baseline.\n                  <\/jats:p>","DOI":"10.1145\/3742465","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"1540-1564","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["AWDIT: An Optimal Weak Database Isolation Tester"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-9670-7039","authenticated-orcid":false,"given":"Lasse","family":"M\u00f8ldrup","sequence":"first","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8943-0722","authenticated-orcid":false,"given":"Andreas","family":"Pavlogiannis","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_1","unstructured":"2011. Big Data in Real Time at Twitter. https:\/\/www.infoq.com\/presentations\/Big-Data-in-Real-Time-at-Twitter\/."},{"key":"e_1_3_2_3_1","unstructured":"2024. Causal Consistency and Read and Write Concerns. https:\/\/www.mongodb.com\/docs\/manual\/core\/causal-consistency-read-write-concerns\/."},{"key":"e_1_3_2_4_1","unstructured":"2024. CockroachDB. https:\/\/www.cockroachlabs.com\/docs\/stable\/architecture\/transaction-layer."},{"key":"e_1_3_2_5_1","unstructured":"2024. Consistency levels in Azure Cosmos DB. https:\/\/learn.microsoft.com\/en-us\/azure\/cosmos-db\/consistency-levels."},{"key":"e_1_3_2_6_1","unstructured":"2024. Jepsen: Distributed Systems Safety Research. https:\/\/jepsen.io\/analyses."},{"key":"e_1_3_2_7_1","unstructured":"2024. Neo4j. https:\/\/neo4j.com\/docs\/operations-manual\/current\/clustering\/introduction\/."},{"key":"e_1_3_2_8_1","unstructured":"2024. PostgreSQL. https:\/\/www.postgresql.org\/docs\/current\/transaction-iso.html."},{"key":"e_1_3_2_9_1","unstructured":"2024. RocksDB. https:\/\/github.com\/facebook\/rocksdb\/wiki\/Transactions."},{"key":"e_1_3_2_10_1","unstructured":"2024. TPC-C: An On-Line Transaction Processing Benchmark. https:\/\/www.tpc.org\/tpcc\/default5.asp."},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360576"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDE.2000.839388"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDCS.2016.98"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","unstructured":"ChristianaAmza AnupamChanda Alan L.Cox SamehElnikety RomerGil KarthickRajamani WilyZwaenepoel EmmanuelCecchet and JulieMarguerite. 2002. Specification and Implementation of Dynamic Web Site Benchmarks. In 2002 IEEE International Workshop on Workload Characterization. 3\u201313. https:\/\/doi.org\/10.1109\/WWC.2002.1226489 10.1109\/WWC.2002.1226489","DOI":"10.1109\/WWC.2002.1226489"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2909870"},{"key":"e_1_3_2_16_1","first-page":"13","volume-title":"14th Workshop on Hot Topics in Operating Systems, HotOS XIV","author":"Bailis Peter","year":"2013","unstructured":"Peter Bailis, Alan D. Fekete, Ali Ghodsi, Joseph M. Hellerstein, and Ion Stoica. 2013. HAT, Not CAP: Towards Highly Available Transactions. In 14th Workshop on Hot Topics in Operating Systems, HotOS XIV, Santa Ana Pueblo, New Mexico, USA, May 13\u201315, 2013, Petros Maniatis (Ed.). USENIX Association. https:\/\/www.usenix.org\/conference\/hotos13\/session\/bailis"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","unstructured":"Sam Bayless Noah Bayless Holger Hoos and Alan Hu. 2015. SAT Modulo Monotonic Theories. Proceedings of the AAAI Conference on Artificial Intelligence 29 1 (March 2015). https:\/\/doi.org\/10.1609\/aaai.v29i1.9755 10.1609\/aaai.v29i1.9755","DOI":"10.1609\/aaai.v29i1.9755"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/568271.223785"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360591"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009888"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485541"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","unstructured":"Sebastian Burckhardt Alexey Gotsman Hongseok Yang and Marek Zawirski. 2014. Replicated Data Types: Specification Verification Optimality. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. (San Diego California USA) (POPL \u201914)Association for Computing Machinery New York NY USA 271\u2013284. https:\/\/doi.org\/10.1145\/2535838.2535848 10.1145\/2535838.2535848","DOI":"10.1145\/2535838.2535848"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","unstructured":"AndreaCerone GiovanniBernardi and AlexeyGotsman. 2015. A Framework for Transactional Consistency Models with Atomic Visibility. In DROPS-IDN\/v2\/Document\/10.4230\/LIPIcs.CONCUR.2015.58. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik. https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2015.58 10.4230\/LIPIcs.CONCUR.2015.58","DOI":"10.4230\/LIPIcs.CONCUR.2015.58"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632908"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158119"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.14778\/3476311.3476379"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1137\/0211038"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","unstructured":"NatachaCrooks YouerPu LorenzoAlvisi 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 \u201917). Association for Computing Machinery New York NY USA 73\u201382. https:\/\/doi.org\/10.1145\/3087801.3087802 10.1145\/3087801.3087802","DOI":"10.1145\/3087801.3087802"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.14778\/3236187.3236210"},{"key":"e_1_3_2_31_1","unstructured":"Mattern Friedemann. 1989. Virtual Time and Global States of Distributed Systems. In Proceedings of the International Workshop on Parallel & Distributed Algorithms. Elsevier Science Publishers B. V. 215\u2013226."},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2753761"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","unstructured":"Chujun Geng Spyros Blanas Michael D. Bond and YangWang. 2024. IsoPredict: Dynamic Predictive Analysis for Detecting Unserializable Behaviors in Weakly Isolated Data Store Applications. Proceedings of the ACM on Programming Languages 8 PLDI June. https:\/\/doi.org\/10.1145\/3656391 10.1145\/3656391","DOI":"10.1145\/3656391"},{"key":"e_1_3_2_34_1","doi-asserted-by":"crossref","unstructured":"Phillip B. Gibbons Ephraim Korach. 1994. On testing cache-coherent shared memories. Proceedings of the Sixth Annual ACM Symposium on Parallel Algorithms and Architectures 177\u2013188.","DOI":"10.1145\/181014.181328"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539794279614"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.14778\/3583140.3583145"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","unstructured":"KyleKingsbury PeterAlvaro 2020. Elle: Inferring Isolation Anomalies from Experimental Observations. Proceedings of the VLDB Endowment 14 3 (Nov. 2020) 268\u2013280. https:\/\/doi.org\/10.14778\/3430915.3430918 10.14778\/3430915.3430918","DOI":"10.14778\/3430915.3430918"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","unstructured":"OriLahav and Viktor Vafeiadis 2015. Owicki-Gries Reasoning for Weak Memory Models. In Automata Languages and Programming Magn\u00fas M.Halld\u00f3rsson Kazuo Iwama Naoki Kobayashi and Bettina Speckmann (Eds.). 9135 Springer Berlin Heidelberg Berlin Heidelberg 311 323. https:\/\/doi.org\/10.1007\/978-3-662-47666-6_25 10.1007\/978-3-662-47666-6_25","DOI":"10.1007\/978-3-662-47666-6_25"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689742"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3503222.3507734"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","unstructured":"UmangMathur Andreas Pavlogiannis MaheshViswanathan 2020. The Complexity of Dynamic Data Race Prediction. Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science ACM 713 727. https:\/\/doi.org\/10.1145\/3373718.3394783 10.1145\/3373718.3394783","DOI":"10.1145\/3373718.3394783"},{"key":"e_1_3_2_42_1","unstructured":"SyedAkbar CodyLyttle LorenzoAlvisi Nathan Bronson WyattLloyd 2017. I can\u2019t believe it\u2019s not causal! Scalable causal consistency with no slowdown cascades. In Proceedings of the 14th USENIX Conference on Networked Systems Design and Implementation USENIX Association 453 468"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","unstructured":"LasseM\u00f8ldrup Andreas Pavlogiannis 2025a. Artifact for \"AWDIT: An Optimal Weak Database Isolation Tester\". arXiv:2504.06975[cs.PL] https: \/\/doi.org\/10.5281\/zenodo.15170736 10.5281\/zenodo.15170736","DOI":"10.5281\/zenodo.15170736"},{"key":"e_1_3_2_44_1","article-title":"AWDIT: An Optimal Weak Database Isolation Tester.","author":"M\u00f8ldrup Lasse","year":"2025","unstructured":"Lasse M\u00f8ldrup Andreas Pavlogiannis 2025b. AWDIT: An Optimal Weak Database Isolation Tester. arXiv 2504.06975 [cs.PL] https:\/\/arxiv.org\/abs\/2504.06975","journal-title":"arXiv"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/322154.322158"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3035918.3056096"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","unstructured":"Andreas Pavlogiannis 2020. Fast Sound and Effectively Complete Dynamic Race Prediction. Proceedings of the ACM on Programming Languages 4 POPL (Jan.2020) 1 29 https:\/\/doi.org\/10.1145\/3035918.3056096 10.1145\/3371085","DOI":"10.1145\/3371085"},{"key":"e_1_3_2_48_1","unstructured":"Cheng Tan Changpeng Zhao Shuai Mu and Michael Walsh. 2020. Cobra: Making Transactional Key-Value Stores Verifiably Serializable. 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2020) USENIX Association November 4\u20136 63 80 https:\/\/www.usenix.org\/conference\/osdi20\/presentation\/tan"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","unstructured":"D. B. Terry A. J. Demers K. Petersen M. J. Spreitzer M. M. Theimer and B. B. Welch. 1994. Session Guarantees for Weakly Consistent Replicated Data. In Proceedings of 3rd International Conference on Parallel and Distributed Information Systems 140\u2013149. https:\/\/doi.org\/10.1109\/PDIS.1994.331722 10.1109\/PDIS.1994.331722","DOI":"10.1109\/PDIS.1994.331722"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","unstructured":"Hi\u0144kar Can Tun\u00e7 Parosh Aziz Abdulla Soham Chakraborty Shankaranarayan Krishna Umang Mathur and Andreas Pavlogiannis. 2023. Optimal Reads-From Consistency Checking for C11-Style Memory Models. Proceedings of the ACM on Programming Languages (PLDI) 7 (June 2023) 137\u2013785 https:\/\/doi.org\/10.1145\/3591251 10.1145\/3591251","DOI":"10.1145\/3591251"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3620666.3651358"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","unstructured":"Virginia Vassilevska Williams. 2019. On Some Fine-Grained Questions in Algorithms and Complexity. 3447\u20133487 https:\/\/doi.org\/10.1142\/9789813272880_0188 10.1142\/S9789813272880_0188","DOI":"10.1142\/S9789813272880_0188"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3186893"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/512644.512661"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00607-021-00911-3"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","unstructured":"Jian Zhang Ye Ji Shuai Mu and Cheng Tan. 2023. Viper: A Fast Snapshot Isolation Checker. Proceedings of the Eighteenth European Conference on Computer Systems (EuroSys \u201923) Association for Computing Machinery New York NY USA 654\u2013671 https:\/\/doi.org\/10.1145\/3552326.3567492 10.1145\/3552326.3567492","DOI":"10.1145\/3552326.3567492"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3742465","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:07:48Z","timestamp":1784196468000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3742465"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":55,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3742465"],"URL":"https:\/\/doi.org\/10.1145\/3742465","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}