{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:34:02Z","timestamp":1767929642627,"version":"3.49.0"},"reference-count":62,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T00:00:00Z","timestamp":1686009600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-sa\/4.0\/"}],"funder":[{"name":"French National Research Agency","award":["ANR-19-CE25-0007"],"award-info":[{"award-number":["ANR-19-CE25-0007"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,6,6]]},"abstract":"<jats:p>Modern applications, such as social networking systems and e-commerce platforms are centered around using large-scale databases for storing and retrieving data. Accesses to the database are typically enclosed in transactions that allow computations on shared data to be isolated from other concurrent computations and resilient to failures. Modern databases trade isolation for performance. The weaker the isolation level is, the more behaviors a database is allowed to exhibit and it is up to the developer to ensure that their application can tolerate those behaviors.<\/jats:p><jats:p>In this work, we propose stateless model checking algorithms for studying correctness of such applications that rely on dynamic partial order reduction. These algorithms work for a number of widely-used weak isolation levels, including Read Committed, Causal Consistency, Snapshot Isolation and Serializability. We show that they are complete, sound and optimal, and run with polynomial memory consumption in all cases. We report on an implementation of these algorithms in the context of Java Pathfinder applied to a number of challenging applications drawn from the literature of distributed systems and databases.<\/jats:p>","DOI":"10.1145\/3591243","type":"journal-article","created":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T20:06:24Z","timestamp":1686081984000},"page":"565-590","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Dynamic Partial Order Reduction for Checking Correctness against Transaction Isolation Levels"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2060-3592","authenticated-orcid":false,"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[{"name":"University Paris Cit\u00e9, France \/ CNRS, France \/ IRIF, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2727-8865","authenticated-orcid":false,"given":"Constantin","family":"Enea","sequence":"additional","affiliation":[{"name":"LIX, France \/ \u00c9cole Polytechnique, France \/ CNRS, France \/ Institut Polytechnique de Paris, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-7539-2330","authenticated-orcid":false,"given":"Enrique","family":"Rom\u00e1n-Calvo","sequence":"additional","affiliation":[{"name":"University Paris Cit\u00e9, France \/ CNRS, France \/ IRIF, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,6,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-016-0275-0"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3073408"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360576"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_8"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276505"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/888672"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDE.2000.839388"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_16"},{"key":"e_1_2_1_9_1","unstructured":"Deepthi Devaki Akkoorath and Annette Bieniusa. 2016. Antidote: the highly-available geo-replicated database with strongest guarantees. https:\/\/pages.lip6.fr\/syncfree\/attachments\/article\/59\/antidote-white-paper.pdf Deepthi Devaki Akkoorath and Annette Bieniusa. 2016. Antidote: the highly-available geo-replicated database with strongest guarantees. https:\/\/pages.lip6.fr\/syncfree\/attachments\/article\/59\/antidote-white-paper.pdf"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89963-3_14"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2741948.2741972"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_17"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2019.30"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/223784.223785"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2016.7"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360591"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485546"},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Ahmed Bouajjani Constantin Enea and Enrique Rom\u00e1n-Calvo. 2023. Dynamic Partial Order Reduction for Checking Correctness Against Transaction Isolation Levels. arxiv:2303.12606. Ahmed Bouajjani Constantin Enea and Enrique Rom\u00e1n-Calvo. 2023. Dynamic Partial Order Reduction for Checking Correctness Against Transaction Isolation Levels. arxiv:2303.12606.","DOI":"10.1145\/3591243"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7824546"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation co-located with the 42nd International Symposium on Symbolic and Algebraic Computation (ISSAC","author":"Brain Martin","year":"2017","unstructured":"Martin Brain , James H. Davenport , and Alberto Griggio . 2017. Benchmarking Solvers , SAT-style . In Proceedings of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation co-located with the 42nd International Symposium on Symbolic and Algebraic Computation (ISSAC 2017 ), Kaiserslautern, Germany, July 29, 2017, Matthew England and Vijay Ganesh (Eds.) (CEUR Workshop Proceedings , Vol. 1974). CEUR-WS.org. http:\/\/ceur-ws.org\/Vol-1974\/RP 3 .pdf Martin Brain, James H. Davenport, and Alberto Griggio. 2017. Benchmarking Solvers, SAT-style. In Proceedings of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation co-located with the 42nd International Symposium on Symbolic and Algebraic Computation (ISSAC 2017), Kaiserslautern, Germany, July 29, 2017, Matthew England and Vijay Ganesh (Eds.) (CEUR Workshop Proceedings, Vol. 1974). CEUR-WS.org. http:\/\/ceur-ws.org\/Vol-1974\/RP3.pdf"},{"key":"e_1_2_1_21_1","volume-title":"TAO: Facebook\u2019s Distributed Data Store for the Social Graph. In 2013 USENIX Annual Technical Conference","author":"Bronson Nathan","year":"2013","unstructured":"Nathan Bronson , Zach Amsden , George Cabrera , Prasad Chakka , Peter Dimov , Hui Ding , Jack Ferris , Anthony Giardullo , Sachin Kulkarni , Harry C. Li , Mark Marchukov , Dmitri Petrov , Lovro Puzar , Yee Jiun Song , and Venkateshwaran Venkataramani . 2013 . TAO: Facebook\u2019s Distributed Data Store for the Social Graph. In 2013 USENIX Annual Technical Conference , San Jose, CA, USA , June 26-28, 2013, Andrew Birrell and Emin G\u00fcn Sirer (Eds.). USENIX Association, 49\u201360. https:\/\/www.usenix.org\/conference\/atc13\/technical-sessions\/presentation\/bronson Nathan Bronson, Zach Amsden, George Cabrera, Prasad Chakka, Peter Dimov, Hui Ding, Jack Ferris, Anthony Giardullo, Sachin Kulkarni, Harry C. Li, Mark Marchukov, Dmitri Petrov, Lovro Puzar, Yee Jiun Song, and Venkateshwaran Venkataramani. 2013. TAO: Facebook\u2019s Distributed Data Store for the Social Graph. In 2013 USENIX Annual Technical Conference, San Jose, CA, USA, June 26-28, 2013, Andrew Birrell and Emin G\u00fcn Sirer (Eds.). USENIX Association, 49\u201360. https:\/\/www.usenix.org\/conference\/atc13\/technical-sessions\/presentation\/bronson"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009895"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192415"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2015.58"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3152396"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158119"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360550"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/567067.567080"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050035"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1294261.1294281"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.14778\/2732240.2732246"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1071610.1071615"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.14778\/3407790.3407860"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60761-7"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837625"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the 33rd International Conference on Very Large Data Bases","author":"Jorwekar Sudhir","year":"2007","unstructured":"Sudhir Jorwekar , Alan D. Fekete , Krithi Ramamritham , and S. Sudarshan . 2007. Automating the Detection of Snapshot Isolation Anomalies . In Proceedings of the 33rd International Conference on Very Large Data Bases , University of Vienna, Austria , September 23-27, 2007 , Christoph Koch, Johannes Gehrke, Minos N. Garofalakis, Divesh Srivastava, Karl Aberer, Anand Deshpande, Daniela Florescu, Chee Yong Chan, Venkatesh Ganti, Carl-Christian Kanne, Wolfgang Klas, and Erich J. Neuhold (Eds.). ACM, 1263\u20131274. http:\/\/www.vldb.org\/conf\/2007\/papers\/industrial\/p1263-jorwekar.pdf Sudhir Jorwekar, Alan D. Fekete, Krithi Ramamritham, and S. Sudarshan. 2007. Automating the Detection of Snapshot Isolation Anomalies. In Proceedings of the 33rd International Conference on Very Large Data Bases, University of Vienna, Austria, September 23-27, 2007, Christoph Koch, Johannes Gehrke, Minos N. Garofalakis, Divesh Srivastava, Karl Aberer, Anand Deshpande, Daniela Florescu, Chee Yong Chan, Venkatesh Ganti, Carl-Christian Kanne, Wolfgang Klas, and Erich J. Neuhold (Eds.). ACM, 1263\u20131274. http:\/\/www.vldb.org\/conf\/2007\/papers\/industrial\/p1263-jorwekar.pdf"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276534"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498711"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314609"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373376.3378480"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_2_1_44_1","volume-title":"Automating the Choice of Consistency Levels in Replicated Systems. In 2014 USENIX Annual Technical Conference, USENIX ATC \u201914","author":"Li Cheng","year":"2014","unstructured":"Cheng Li , Jo\u00e3o Leit\u00e3o , Allen Clement , Nuno M. Pregui\u00e7a , Rodrigo Rodrigues , and Viktor Vafeiadis . 2014 . Automating the Choice of Consistency Levels in Replicated Systems. In 2014 USENIX Annual Technical Conference, USENIX ATC \u201914 , Philadelphia, PA, USA , June 19-20, 2014, Garth Gibson and Nickolai Zeldovich (Eds.). USENIX Association, 281\u2013292. https:\/\/www.usenix.org\/conference\/atc14\/technical-sessions\/presentation\/li_cheng_2 Cheng Li, Jo\u00e3o Leit\u00e3o, Allen Clement, Nuno M. Pregui\u00e7a, Rodrigo Rodrigues, and Viktor Vafeiadis. 2014. Automating the Choice of Consistency Levels in Replicated Systems. In 2014 USENIX Annual Technical Conference, USENIX ATC \u201914, Philadelphia, PA, USA, June 19-20, 2014, Garth Gibson and Nickolai Zeldovich (Eds.). USENIX Association, 281\u2013292. https:\/\/www.usenix.org\/conference\/atc14\/technical-sessions\/presentation\/li_cheng_2"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043593"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-17906-2_30"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2018.41"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_20"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509514"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-67087-0_17"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/322154.322158"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3035918.3056096"},{"key":"e_1_2_1_53_1","volume-title":"Microsoft Azure Cosmos DB Revealed: A Multi-Modal Database Designed for the Cloud","author":"Guay Paz Jos Rolando","unstructured":"Jos Rolando Guay Paz . 2018. Microsoft Azure Cosmos DB Revealed: A Multi-Modal Database Designed for the Cloud ( 1 st ed.). Apress , USA. isbn:1484233506 Jos Rolando Guay Paz. 2018. Microsoft Azure Cosmos DB Revealed: A Multi-Modal Database Designed for the Cloud (1st ed.). Apress, USA. isbn:1484233506","edition":"1"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56922-7_34"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-11494-7_22"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360543"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737981"},{"key":"e_1_2_1_58_1","unstructured":"TPC. 2010. Transaction Processing Performance Council. http:\/\/www.tpc.org\/tpc_documents_current_versions\/pdf\/tpc-c_v5.11.0.pdf TPC. 2010. Transaction Processing Performance Council. http:\/\/www.tpc.org\/tpc_documents_current_versions\/pdf\/tpc-c_v5.11.0.pdf"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-53863-1_36"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007512.1007526"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3035918.3064037"},{"key":"e_1_2_1_62_1","unstructured":"ANSI X3. 1992. 135-1992. American National Standard for Information Systems-Database Language-SQL. ANSI X3. 1992. 135-1992. American National Standard for Information Systems-Database Language-SQL."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591243","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3591243","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:47Z","timestamp":1750178867000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591243"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,6]]},"references-count":62,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2023,6,6]]}},"alternative-id":["10.1145\/3591243"],"URL":"https:\/\/doi.org\/10.1145\/3591243","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,6,6]]},"assertion":[{"value":"2023-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}