{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,20]],"date-time":"2025-07-20T04:16:23Z","timestamp":1752984983844,"version":"3.41.0"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"NSF","award":["CCF-2118745,CSR-2106117"],"award-info":[{"award-number":["CCF-2118745,CSR-2106117"]}]},{"name":"Oracle America, Inc","award":["OAC-2112606"],"award-info":[{"award-number":["OAC-2112606"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,6,20]]},"abstract":"<jats:p>\n            Distributed data stores typically provide weak isolation levels, which are efficient but can lead to unserializable behaviors, which are hard for programmers to understand and often result in errors. This paper presents the first dynamic predictive analysis for data store applications under weak isolation levels, called\n            <jats:italic toggle=\"yes\">IsoPredict<\/jats:italic>\n            . Given an observed\n            <jats:italic toggle=\"yes\">serializable<\/jats:italic>\n            execution of a data store application, IsoPredict generates and solves SMT constraints to find an\n            <jats:italic toggle=\"yes\">unserializable<\/jats:italic>\n            execution that is a feasible execution of the application. IsoPredict introduces novel techniques that handle divergent application behavior; solve mutually recursive sets of constraints; and balance coverage, precision, and performance. An evaluation on four transactional data store benchmarks shows that IsoPredict often predicts unserializable behaviors,\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mn>99<\/mml:mn>\n                <mml:mo>%<\/mml:mo>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            of which are feasible.\n          <\/jats:p>","DOI":"10.1145\/3656391","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"343-367","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["IsoPredict: Dynamic Predictive Analysis for Detecting Unserializable Behaviors in Weakly Isolated Data Store Applications"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-6149-0208","authenticated-orcid":false,"given":"Chujun","family":"Geng","sequence":"first","affiliation":[{"name":"Ohio State University, Columbus, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-2703-7177","authenticated-orcid":false,"given":"Spyros","family":"Blanas","sequence":"additional","affiliation":[{"name":"Ohio State University, Columbus, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8971-4944","authenticated-orcid":false,"given":"Michael D.","family":"Bond","sequence":"additional","affiliation":[{"name":"Ohio State University, Columbus, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9721-4923","authenticated-orcid":false,"given":"Yang","family":"Wang","sequence":"additional","affiliation":[{"name":"Ohio State University, Columbus, USA"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30823-9_6"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","unstructured":"A. Adya B. Liskov and P. O'Neil. 2000. Generalized isolation level definitions. In Proceedings of 16th International Conference on Data Engineering (Cat. No.00CB37073). IEEE Computer Society Los Alamitos CA USA 67-78. https:\/\/doi.org\/10.1109\/ICDE.2000.839388 10.1109\/ICDE.2000.839388","DOI":"10.1109\/ICDE.2000.839388"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","unstructured":"Mustaque Ahamad Gil Neiger James E. Burns Prince Kohli and P.W. Hutto. 1995. Causal Memory: Definitions Implementation and Programming. Distributed Computing 9 1 (1995) 37-49. https:\/\/doi.org\/10.1007\/BF01784241 10.1007\/BF01784241","DOI":"10.1007\/BF01784241"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","unstructured":"Jade Alglave Luc Maranget and Michael Tautschnig. 2014. Herding Cats: Modelling Simulation Testing and Data Mining for Weak Memory. ACM Trans. Program. Lang. Syst. 36 2 Article 7 (Jul 2014) 74 pages. https:\/\/doi.org\/10.1145\/2627752 10.1145\/2627752","DOI":"10.1145\/2627752"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","unstructured":"Hal Berenson Phil Bernstein Jim Gray Jim Melton Elizabeth O'Neil and Patrick O'Neil. 1995. A Critique of ANSI SQL Isolation Levels. In Proceedings of the 1995 ACM SIGMOD International Conference on Management of Data (San Jose California USA) (SIGMOD '95). ACM New York NY USA 1-10. https:\/\/doi.org\/10.1145\/223784.223785 10.1145\/223784.223785","DOI":"10.1145\/223784.223785"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","unstructured":"Ranadeep Biswas and Constantin Enea. 2019. On the Complexity of Checking Transactional Consistency. Proc. ACM Program. Lang. 3 OOPSLA Article 165 (Oct 2019) 28 pages. https:\/\/doi.org\/10.1145\/3360591 10.1145\/3360591","DOI":"10.1145\/3360591"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","unstructured":"Ranadeep Biswas Diptanshu Kakwani Jyothi Vedurada Constantin Enea and Akash Lal. 2021. MonkeyDB: Effectively Testing Correctness under Weak Isolation Levels. Proc. ACM Program. Lang. 5 OOPSLA Article 132 (Oct 2021) 27 pages. https:\/\/doi.org\/10.1145\/3485546 10.1145\/3485546","DOI":"10.1145\/3485546"},{"key":"e_1_3_1_9_1","unstructured":"Ranadeep Biswas Diptanshu Kakwani Jyothi Vedurada Constantin Enea and Akash Lal. 2023. Personal communication."},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","unstructured":"Ahmed Bouajjani Constantin Enea Rachid Guerraoui and Jad Hamza. 2017. On verifying causal consistency. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Paris France) (POPL '17) Association for Computing Machinery New York NY USA 626-638. https:\/\/doi.org\/10.1145\/3009837.3009888 10.1145\/3009837.3009888","DOI":"10.1145\/3009837.3009888"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","unstructured":"Ahmed Bouajjani Constantin Enea and Enrique Rom\u00e1n-Calvo. 2023. Dynamic Partial Order Reduction for Checking Correctness against Transaction Isolation Levels. Proc. ACM Program. Lang. 7 PLDI Article 129 (Jun 2023) 26 pages https:\/\/doi.org\/10.1145\/3591243 10.1145\/3591243","DOI":"10.1145\/3591243"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","unstructured":"Lucas Brutschy Dimitar Dimitrov Peter M\u00fcller and Martin Vechev. 2017. Serializability for Eventual Consistency Criterion Analysis and Applications. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Paris France) (POPL '17). Association for Computing Machinery New York NY USA 458-472. https:\/\/doi.org\/10.1145\/3009837.3009895 10.1145\/3009837.3009895","DOI":"10.1145\/3009837.3009895"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","unstructured":"Lucas Brutschy Dimitar Dimitrov Peter M\u00fcller and Martin Vechev. 2018. Static Serializability Analysis for Causal Consistency. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (Philadelphia PA USA) (PLDI 2018). Association for Computing Machinery New York NY USA 90-104. https:\/\/doi.org\/10.1145\/3192366.3192415 10.1145\/3192366.3192415","DOI":"10.1145\/3192366.3192415"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","unstructured":"Sebastian Burckhardt. 2014. Principles of Eventual Consistency. Found. Trends Program. Lang. 1 1-2 (oct 2014) 1-150 https:\/\/doi.org\/10.1561\/2500000011 10.1561\/2500000011","DOI":"10.1561\/2500000011"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2015.58"},{"key":"e_1_3_1_16_1","unstructured":"Chaoyi Cheng Mingzhe Han Nuo Xu Spyros Blanas Michael D. Bond and Yang Wang. 2023. Developer\u2019s Responsibility or Database\u2019s Responsibility? Rethinking Concurrency Control in Databases. In 13th Conference on Innovative Data Systems Research CIDR 2023 Amsterdam The Netherlands January 8-11 2023. https:\/\/www.cidrdb.org\/cidr2023\/papers\/p30-cheng.pdf"},{"key":"e_1_3_1_17_1","unstructured":"James C. Corbett Jeffrey Dean Michael Epstein Andrew Fikes Christopher Frost JJ Furman Sanjay Ghemawat Andrey Gubarev Christopher Heiser Peter Hochschild Wilson Hsieh Sebastian Kanthak Eugene Kogan Hongyi Li"},{"key":"e_1_3_1_18_1","first-page":"261","volume-title":"In 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI 12)","author":"Lloyd Alexander","year":"2012","unstructured":"[17] Alexander Lloyd, Sergey Melnik, David Mwaura, David Nagle, Sean Quinlan, Rajesh Rao, Lindsay Rolig, Yasushi Saito, Michal Szymaniak, Christopher Taylor, Ruth Wang, and Dale Woodford. 2012. Spanner: Google\u2019s Globally-Distributed Database. In 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI 12). USENIX Association, Hollywood, CA, 261-264. https:\/\/www.usenix.org\/conference\/osdi12\/technical-sessions\/presentation\/corbett"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","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 (Washington DC USA) (PODC '17). ACM New York NY USA 73-82. https:\/\/doi.org\/10.1145\/3087801.3087802 10.1145\/3087801.3087802","DOI":"10.1145\/3087801.3087802"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","unstructured":"Djellel Eddine Difallah Andrew Pavlo Carlo Curino and Philippe Cudre-Mauroux. 2013. OLTP-Bench: An Extensible Testbed for Benchmarking Relational Databases. Proc. VLDB Endow. 7 4 (Dec 2013) 277-288. https:\/\/doi.org\/10.14778\/2732240.2732246 10.14778\/2732240.2732246","DOI":"10.14778\/2732240.2732246"},{"key":"e_1_3_1_22_1","first-page":"1037","volume-title":"USENIX Annual Technical Conference (USENIX ATC 22)","year":"2022","unstructured":"Mostafa Elhemali, Niall Gallagher, Nick Gordon, Joseph Idziorek, Richard Krog, Colin Lazier, Erben Mo, Akhilesh Mritunjai, Somasundaram Perianayagam, Tim Rath, Swami Sivasubramanian, James Christopher Sorenson III, Sroaj Sosothikul, Doug Terry, and Akshat Vig. 2022. Amazon DynamoDB: A Scalable, Predictably Performant, and Fully Managed NoSQL Database Service. In 2022 USENIX Annual Technical Conference (USENIX ATC 22). USENIX Association, Carlsbad, CA, 1037-1048. https:\/\/www.usenix.org\/conference\/atc22\/presentation\/elhemali"},{"key":"e_1_3_1_23_1","unstructured":"Ben Frederickson. 2024. https:\/\/github.com\/benfred\/py-spy"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","unstructured":"Leonidas Galanis Supiti Buranawatanachoke Romain Colle Beno\u00eet Dageville Karl Dias Jonathan Klein Stratos Papadomanolakis Leng Leng Tan Venkateshwaran Venkataramani Yujun Wang and Graham Wood. 2008. Oracle Database Replay. In Proceedings of the 2008 ACM SIGMOD International Conference on Management of Data (Vancouver Canada) (SIGMOD '08). Association for Computing Machinery New York NY USA 1159-1170. https:\/\/doi.org\/10.1145\/1376616.1376732 10.1145\/1376616.1376732","DOI":"10.1145\/1376616.1376732"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.14778\/3407790.3407860"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","unstructured":"Chujun Geng Spyros Blanas Michael D. Bond and Yang Wang. 2024. IsoPredict artifact. https:\/\/doi.org\/10.5281\/zenodo.10802748 10.5281\/zenodo.10802748","DOI":"10.5281\/zenodo.10802748"},{"key":"e_1_3_1_27_1","doi-asserted-by":"crossref","unstructured":"Chujun Geng Spyros Blanas Michael D. Bond and Yang Wang. 2024. IsoPredict: Dynamic Predictive Analysis for Detecting unserializable Behaviors in Weakly Isolated Data Store Applications. arXiv:2404.04621 Extended version of PLDI 2024 paper.","DOI":"10.1145\/3656391"},{"key":"e_1_3_1_28_1","unstructured":"Chujun Geng Spyros Blanas Michael D. Bond and Yang Wang. 2024. IsoPredict implementation. https:\/\/github.com\/PLaSSticity\/IsoPredict-implementation"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2016.25"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","unstructured":"Seth Gilbert and Nancy Lynch. 2002. Brewer\u2019s conjecture and the feasibility of consistent available partition-tolerant web services. SIGACT News 33 (June 2002) 51-59. Issue 2. https:\/\/doi.org\/10.1145\/564585.564601 10.1145\/564585.564601","DOI":"10.1145\/564585.564601"},{"key":"e_1_3_1_31_1","unstructured":"Jad Hamza. 2015. Algorithmic Verification of Concurrent and Distributed Data Structures. Ph. D. Dissertation. PhD thesis Universit\u00e9 Paris Diderot."},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","unstructured":"Jeff Huang Patrick O'Neil Meredith and Grigore Rosu. 2014. Maximal sound predictive race detection with control flow abstraction. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (Edinburgh United Kingdom) (PLDI '14). Association for Computing Machinery New York NY USA 337-348. https:\/\/doi.org\/10.1145\/2594291.2594315 10.1145\/2594291.2594315","DOI":"10.1145\/2594291.2594315"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","unstructured":"Gowtham Kaki Kapil Earanky KC Sivaramakrishnan and Suresh Jagannathan. 2018. Safe replication through bounded concurrency verification. Proc. ACM Program. Lang. 2 OOPSLA Article 164 (Oct 2018) 27 pages. https:\/\/doi.org\/10.1145\/3276534 10.1145\/3276534","DOI":"10.1145\/3276534"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.14778\/3430915.3430918"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062374"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_20"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.14778\/3611479.3611510"},{"key":"e_1_3_1_38_1","volume-title":"Consistency, Availability, Convergence","author":"Mahajan P.","year":"2011","unstructured":"P. Mahajan, L. Alvisi, and M. Dahlin. 2011. Consistency, Availability, Convergence. Technical Report TR-11-22. Computer Science Department, University of Texas at Austin."},{"key":"e_1_3_1_39_1","unstructured":"MySQL 2023. http:\/\/www.mysql.com"},{"key":"e_1_3_1_40_1","unstructured":"MySQL 2023. MySQL Cluster. https:\/\/www.mysql.com\/products\/cluster\/"},{"key":"e_1_3_1_41_1","unstructured":"Kartik Nagar and Suresh Jagannathan. 2018. Automated Detection of Serializability Violations under Weak Consistency. arXiv:1806.08416 [cs.PL]"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","unstructured":"Andrew Pavlo. 2017. What Are We Doing With Our Lives? Nobody Cares About Our Concurrency Control Research. In Proceedings of the 2017 ACM International Conference on Management of Data (Chicago Illinois USA) (SIGMOD '17). Association for Computing Machinery New York NY USA 3. https:\/\/doi.org\/10.1145\/3035918.3056096 10.1145\/3035918.3056096","DOI":"10.1145\/3035918.3056096"},{"key":"e_1_3_1_43_1","unstructured":"perf 2024. https:\/\/perf.wiki.kernel.org\/index.php\/Main_Page"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","unstructured":"Matthieu Perrin Achour Mostefaoui and Claude Jard. 2016. Causal Consistency: Beyond Memory. In Proceedings of the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (Barcelona Spain) (PPoPP '16). Association for Computing Machinery New York NY USA Article 26 12 pages. https:\/\/doi.org\/10.1145\/2851141.2851170 10.1145\/2851141.2851170","DOI":"10.1145\/2851141.2851170"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","unstructured":"Kia Rahmani Kartik Nagar Benjamin Delaware and Suresh Jagannathan. 2019. CLOTHO: Directed Test Generation for Weakly Consistent Database Systems. Proc. ACM Program. Lang. 3 OOPSLA Article 117 (Oct 2019) 28 pages https:\/\/doi.org\/10.1145\/3360543 10.1145\/3360543","DOI":"10.1145\/3360543"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385993"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_23"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","unstructured":"Arnab Sinha Sharad Malik Chao Wang and Aarti Gupta. 2012. Predicting Serializability Violations: SMT-Based Search vs. DPOR-Based Search. In Hardware and Software: Verification and Testing Kerstin Eder Jo\u00e3o Louren\u00e7o and Onn Shehory (Eds.). Springer Berlin Heidelberg Berlin Heidelberg 95-114. https:\/\/doi.org\/10.1007\/978-3-642-34188-5_11 10.1007\/978-3-642-34188-5_11","DOI":"10.1007\/978-3-642-34188-5_11"},{"key":"e_1_3_1_49_1","unstructured":"Snowflake 2023. Snowflake transactions. https:\/\/docs.snowflake.com\/en\/sql-reference\/transactions"},{"key":"e_1_3_1_50_1","unstructured":"Cheng Tan Changgeng Zhao Shuai Mu and Michael Walfish. 2020. COBRA: making transactional key-value stores verifiably serializable. In Proceedings of the 14th USENIX Conference on Operating Systems Design and Implementation (OSDI'20). USENIX Association USA Article 4 18 pages. https:\/\/www.usenix.org\/conference\/osdi20\/presentation\/tan"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3514221.3526120"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","unstructured":"H\u00fcnkar Can Tun\u00e7 Umang Mathur Andreas Pavlogiannis and Mahesh Viswanathan. 2023. Sound Dynamic Deadlock Prediction in Linear Time. Proc. ACM Program. Lang. 7 PLDI Article 177 (Jun 2023) 26 pages. https:\/\/doi.org\/10.1145\/3591291 10.1145\/3591291","DOI":"10.1145\/3591291"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","unstructured":"Todd Warszawski and Peter Bailis. 2017. ACIDRain: Concurrency-Related Attacks on Database-Backed Web Applications. In Proceedings of the 2017 ACM International Conference on Management of Data (Chicago Illinois USA) (SIGMOD \u201917). ACM New York NY USA 5-20. https:\/\/doi.org\/10.1145\/3035918.3064037 10.1145\/3035918.3064037","DOI":"10.1145\/3035918.3064037"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00607-021-00911-3"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","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\/10.1145\/3656391","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656391","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:39:41Z","timestamp":1751661581000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656391"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":54,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656391"],"URL":"https:\/\/doi.org\/10.1145\/3656391","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}