{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T21:05:18Z","timestamp":1776373518881,"version":"3.51.2"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100006602","name":"Air Force Research Lab","doi-asserted-by":"crossref","award":["FA8750-17-1-0006"],"award-info":[{"award-number":["FA8750-17-1-0006"]}],"id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-SHF 1717741"],"award-info":[{"award-number":["CCF-SHF 1717741"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,10,10]]},"abstract":"<jats:p>Relational database applications are notoriously difficult to test and debug. Concurrent execution of database transactions may violate complex structural invariants that constraint how changes to the contents of one (shared) table affect the contents of another. Simplifying the underlying concurrency model is one way to ameliorate the difficulty of understanding how concurrent accesses and updates can affect database state with respect to these sophisticated properties. Enforcing serializable execution of all transactions achieves this simplification, but it comes at a significant price in performance, especially at scale, where database state is often replicated to improve latency and availability.<\/jats:p><jats:p>To address these challenges, this paper presents a novel testing framework for detecting serializability violations in (SQL) database-backed Java applications executing on weakly-consistent storage systems. We manifest our approach in a tool, CLOTHO, that combines a static analyzer and model checker to generate abstract executions, discover serializability violations in these executions, and translate them back into concrete test inputs suitable for deployment in a test environment. To the best of our knowledge, CLOTHO, is the first automated test generation facility for identifying serializability anomalies of Java applications intended to operate in geo-replicated distributed environments. An experimental evaluation on a set of industry-standard benchmarks demonstrates the utility of our approach.<\/jats:p>","DOI":"10.1145\/3360543","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T14:53:33Z","timestamp":1570805613000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["CLOTHO: directed test generation for weakly consistent database systems"],"prefix":"10.1145","volume":"3","author":[{"given":"Kia","family":"Rahmani","sequence":"first","affiliation":[{"name":"Purdue University, USA"}]},{"given":"Kartik","family":"Nagar","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}]},{"given":"Benjamin","family":"Delaware","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}]},{"given":"Suresh","family":"Jagannathan","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"http:\/\/www.tpc.org\/tpc_documents_current_versions\/pdf\/tpc-c_v5.11.0.pdf . Online","author":"Benchmark TPC-C","year":"2019","unstructured":"2010. TPC-C Benchmark . http:\/\/www.tpc.org\/tpc_documents_current_versions\/pdf\/tpc-c_v5.11.0.pdf . Online ; Accessed April 2019 . 2010. TPC-C Benchmark. http:\/\/www.tpc.org\/tpc_documents_current_versions\/pdf\/tpc-c_v5.11.0.pdf . Online; Accessed April 2019."},{"key":"e_1_2_2_2_1","unstructured":"Atul Adya. 1999. Weak Consistency: A Generalized Theory and Optimistic Implementations for Distributed Transactions. Ph.D. Dissertation. Cambridge MA USA. AAI0800775. Atul Adya. 1999. Weak Consistency: A Generalized Theory and Optimistic Implementations for Distributed Transactions. Ph.D. Dissertation. Cambridge MA USA. AAI0800775."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDE.2000.839388"},{"key":"e_1_2_2_4_1","volume-title":"CIDR 2011, Fifth Biennial Conference on Innovative Data Systems Research, Asilomar, CA, USA, January 9-12, 2011, Online Proceedings . 249\u2013260","author":"Alvaro Peter","unstructured":"Peter Alvaro , Neil Conway , Joe Hellerstein , and William R. Marczak . 2011. Consistency Analysis in Bloom: a CALM and Collected Approach . In CIDR 2011, Fifth Biennial Conference on Innovative Data Systems Research, Asilomar, CA, USA, January 9-12, 2011, Online Proceedings . 249\u2013260 . Peter Alvaro, Neil Conway, Joe Hellerstein, and William R. Marczak. 2011. Consistency Analysis in Bloom: a CALM and Collected Approach. In CIDR 2011, Fifth Biennial Conference on Innovative Data Systems Research, Asilomar, CA, USA, January 9-12, 2011, Online Proceedings . 249\u2013260."},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.14778\/2735508.2735509"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2588555.2588562"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2741948.2741972"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/223784.223785"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2016.7"},{"key":"e_1_2_2_10_1","unstructured":"Blockade. 2019. Blockade. https:\/\/github.com\/worstcase\/blockade accessed on 2019-03-29. Blockade. 2019. Blockade. https:\/\/github.com\/worstcase\/blockade accessed on 2019-03-29."},{"key":"e_1_2_2_11_1","volume-title":"Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017","author":"Brutschy Lucas","year":"2017","unstructured":"Lucas Brutschy , Dimitar Dimitrov , Peter M\u00fcller , and Martin T. Vechev . 2017. Serializability for eventual consistency: criterion, analysis, and applications . In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017 , Paris, France , January 18-20, 2017 . 458\u2013472. http:\/\/dl.acm.org\/citation.cfm?id=3009895 Lucas Brutschy, Dimitar Dimitrov, Peter M\u00fcller, and Martin T. Vechev. 2017. Serializability for eventual consistency: criterion, analysis, and applications. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017 . 458\u2013472. http:\/\/dl.acm.org\/citation.cfm?id=3009895"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192415"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535848"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2015.58"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933057.2933096"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2017.26"},{"key":"e_1_2_2_17_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"de Moura Leonardo","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner . 2008. Z3: An Efficient SMT Solver . In Tools and Algorithms for the Construction and Analysis of Systems , C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 337\u2013340. Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems , C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 337\u2013340."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.14778\/2732240.2732246"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1071610.1071615"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964023"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781169"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837625"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368120"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462167"},{"key":"e_1_2_2_25_1","doi-asserted-by":"crossref","unstructured":"Jepsen 2018. https:\/\/jepsen.io\/ Jepsen 2018. https:\/\/jepsen.io\/","DOI":"10.1063\/pt.6.4o.20181207a"},{"key":"e_1_2_2_26_1","volume-title":"Proceedings of the 33rd International Conference on Very Large Data Bases","author":"Jorwekar Sudhir","year":"2007","unstructured":"Sudhir Jorwekar , Alan 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 . 1263\u20131274. http:\/\/www.vldb.org\/conf\/2007\/papers\/industrial\/p1263-jorwekar.pdf Sudhir Jorwekar, Alan 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 . 1263\u20131274. http:\/\/www.vldb.org\/conf\/2007\/papers\/industrial\/p1263-jorwekar.pdf"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276534"},{"key":"e_1_2_2_28_1","volume-title":"Proceedings of the 4th USENIX Conference on Networked Systems Design &amp;#38; Implementation (NSDI\u201907)","author":"Killian Charles","year":"2007","unstructured":"Charles Killian , James W. Anderson , Ranjit Jhala , and Amin Vahdat . 2007 . Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code . In Proceedings of the 4th USENIX Conference on Networked Systems Design &amp;#38; Implementation (NSDI\u201907) . USENIX Association, Berkeley, CA, USA, 18\u201318. http:\/\/dl.acm.org\/citation.cfm?id= 1973430. 1973448 Charles Killian, James W. Anderson, Ranjit Jhala, and Amin Vahdat. 2007. Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code. In Proceedings of the 4th USENIX Conference on Networked Systems Design &amp;#38; Implementation (NSDI\u201907) . USENIX Association, Berkeley, CA, USA, 18\u201318. http:\/\/dl.acm.org\/citation.cfm?id=1973430. 1973448"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837622"},{"key":"e_1_2_2_30_1","volume-title":"Proceedings of USENIX Annual Technical Conference (USENIX ATC\u201914)","author":"Li Cheng","year":"2014","unstructured":"Cheng Li , Jo\u00e3o Leit\u00e3o , Allen Clement , Nuno Pregui\u00e7a , Rodrigo Rodrigues , and Viktor Vafeiadis . 2014 . Automating the Choice of Consistency Levels in Replicated Systems . In Proceedings of USENIX Annual Technical Conference (USENIX ATC\u201914) . USENIX Association, Berkeley, CA, USA, 281\u2013292. http:\/\/dl.acm.org\/citation.cfm?id=2643634.2643664 Cheng Li, Jo\u00e3o Leit\u00e3o, Allen Clement, Nuno Pregui\u00e7a, Rodrigo Rodrigues, and Viktor Vafeiadis. 2014. Automating the Choice of Consistency Levels in Replicated Systems. In Proceedings of USENIX Annual Technical Conference (USENIX ATC\u201914) . USENIX Association, Berkeley, CA, USA, 281\u2013292. http:\/\/dl.acm.org\/citation.cfm?id=2643634.2643664"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/2387880.2387906"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1294261.1294272"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168864"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1815961.1815988"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737973"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111068"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2018.41"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/322154.322158"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3194261.3194267"},{"key":"e_1_2_2_40_1","volume-title":"CLOTHO: Directed Test Generation for Weakly Consistent Database Systtems (Extended Version). https:\/\/arxiv.org\/pdf\/1908.05655.pdf","author":"Rahmani Kia","year":"2019","unstructured":"Kia Rahmani , Kartik Nagar , Benjamin Delaware , and Suresh Jagannatha . 2019 . CLOTHO: Directed Test Generation for Weakly Consistent Database Systtems (Extended Version). https:\/\/arxiv.org\/pdf\/1908.05655.pdf Kia Rahmani, Kartik Nagar, Benjamin Delaware, and Suresh Jagannatha. 2019. CLOTHO: Directed Test Generation for Weakly Consistent Database Systtems (Extended Version). https:\/\/arxiv.org\/pdf\/1908.05655.pdf"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1508244.1508266"},{"key":"e_1_2_2_42_1","volume-title":"Database Tuning: Principles, Experiments, and Troubleshooting Techniques","author":"Shasha Dennis","year":"2003","unstructured":"Dennis Shasha and Philippe Bonnet . 2003 . Database Tuning: Principles, Experiments, and Troubleshooting Techniques . Morgan Kaufmann Publishers Inc ., San Francisco, CA, USA. Dennis Shasha and Philippe Bonnet. 2003. Database Tuning: Principles, Experiments, and Troubleshooting Techniques. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA."},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737981"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183713.3196893"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/781995.782008"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3035918.3064037"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065013"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2522729"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360543","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360543","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360543","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:22:58Z","timestamp":1750202578000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360543"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":48,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360543"],"URL":"https:\/\/doi.org\/10.1145\/3360543","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"2019-10-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}