{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T08:42:58Z","timestamp":1777106578471,"version":"3.51.4"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2020,11,13]],"date-time":"2020-11-13T00:00:00Z","timestamp":1605225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100011199","name":"European Research Council","doi-asserted-by":"publisher","award":["610150, 678177"],"award-info":[{"award-number":["610150, 678177"]}],"id":[{"id":"10.13039\/100011199","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100008952","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["SAFTA 12744-ANR-17-CE25-0008-01"],"award-info":[{"award-number":["SAFTA 12744-ANR-17-CE25-0008-01"]}],"id":[{"id":"10.13039\/501100008952","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["389792660 TRR 248--CPEC"],"award-info":[{"award-number":["389792660 TRR 248--CPEC"]}],"id":[{"id":"10.13039\/501100001659","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":[[2020,11,13]]},"abstract":"<jats:p>\n            Large scale production distributed systems are difficult to design and test. Correctness must be ensured when processes run asynchronously, at arbitrary rates relative to each other, and in the presence of failures, e.g., process crashes or message losses. These conditions create a huge space of executions that is difficult to explore in a principled way. Current testing techniques focus on systematic or randomized exploration of all executions of an implementation while treating the implemented algorithms as black boxes. On the other hand, proofs of correctness of many of the underlying algorithms often exploit semantic properties that reduce reasoning about correctness to a subset of behaviors. For example, the\n            <jats:italic>communication-closure<\/jats:italic>\n            property, used in many proofs of distributed consensus algorithms, shows that every asynchronous execution of the algorithm is equivalent to a\n            <jats:italic>lossy synchronous<\/jats:italic>\n            execution, thus reducing the burden of proof to only that subset. In a lossy synchronous execution, processes execute in lock-step rounds, and messages are either received in the same round or lost forever\u2014such executions form a small subset of all asynchronous ones.\n          <\/jats:p>\n          <jats:p>\n            We formulate the\n            <jats:italic>communication-closure hypothesis<\/jats:italic>\n            , which states that bugs in implementations of distributed consensus algorithms will already manifest in lossy synchronous executions and present a testing algorithm based on this hypothesis. We prioritize the search space based on a bound on the number of failures in the execution and the rate at which these failures are recovered. We show that a random testing algorithm based on sampling lossy synchronous executions can empirically find a number of bugs\u2014including previously unknown ones\u2014in production distributed systems such as Zookeeper, Cassandra, and Ratis, and also produce more understandable bug traces.\n          <\/jats:p>","DOI":"10.1145\/3428278","type":"journal-article","created":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T23:36:06Z","timestamp":1606260966000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Testing consensus implementations using communication closure"],"prefix":"10.1145","volume":"4","author":[{"given":"Cezara","family":"Dr\u0103goi","sequence":"first","affiliation":[{"name":"Inria, France \/ Informal Systems, France"}]},{"given":"Constantin","family":"Enea","sequence":"additional","affiliation":[{"name":"University of Paris, France \/ IRIF, France \/ CNRS, France"}]},{"given":"Burcu Kulahcioglu","family":"Ozkan","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2136-0542","authenticated-orcid":false,"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]},{"given":"Filip","family":"Niksic","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}]}],"member":"320","published-online":{"date-parts":[[2020,11,13]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Retrieved","year":"2013"},{"key":"e_1_2_2_2_1","volume-title":"Retrieved","year":"2020"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/122120.122133"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/41457.37515"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1736020.1736040"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1281100.1281103"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04420-5_10"},{"key":"e_1_2_2_8_1","doi-asserted-by":"crossref","volume-title":"Enumerative combinatorics","author":"Charalambides Charalambos A","DOI":"10.1201\/9781315273112"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-009-0084-6"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_12"},{"key":"e_1_2_2_11_1","unstructured":"Ching-Tsun Chou and Eli Gafni. 1988. Understanding and Verifying Distributed Algorithms Using Stratified Decomposition.  Ching-Tsun Chou and Eli Gafni. 1988. Understanding and Verifying Distributed Algorithms Using Stratified Decomposition."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/62546.62556"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_20"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786861"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837650"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/42282.42283"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(83)90013-8"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926432"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0039061"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3149.214121"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3064176.3064183"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/277697.277724"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236030"},{"key":"e_1_2_2_24_1","volume-title":"Suminto","author":"Gunawi Haryadi S.","year":"2015"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_2_2_26_1","volume-title":"ZooKeeper: Wait-free Coordination for Internet-scale Systems. In 2010 USENIX Annual Technical Conference","author":"Hunt Patrick","year":"2010"},{"key":"e_1_2_2_27_1","unstructured":"Yury Izrailevsky and Ariel Tseitlin. 2011. The Netflix Simian army. The Netflix Tech Blog ( 2011 ).  Yury Izrailevsky and Ariel Tseitlin. 2011. The Netflix Simian army. The Netflix Tech Blog ( 2011 )."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2011.5958223"},{"key":"e_1_2_2_29_1","volume-title":"Quantum calculus","author":"Kac Victor"},{"key":"e_1_2_2_30_1","volume-title":"4th Symposium on Networked Systems Design and Implementation (NSDI 2007 )","author":"Killian Charles Edwin","year":"2007"},{"key":"e_1_2_2_31_1","volume-title":"Jepsen. Retrieved","author":"Kingsbury Kyle","year":"2013"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1773912.1773922"},{"key":"e_1_2_2_34_1","volume-title":"SAMC: Semantic-Aware Model Checking for Fast Discovery of Deep Bugs in Cloud Systems. In 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI '14","author":"Leesatapornwongsa Tanakorn","year":"2014"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359645"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3302424.3303986"},{"key":"e_1_2_2_37_1","volume-title":"Distributed Algorithms","author":"Lynch Nancy A."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2517350"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539799364006"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250785"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/62546.62549"},{"key":"e_1_2_2_42_1","volume-title":"2014 USENIX Annual Technical Conference, USENIX ATC '14","author":"Ongaro Diego","year":"2014"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276530"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360606"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140568"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028994"},{"key":"e_1_2_2_48_1","volume-title":"On the correctness of Egalitarian Paxos. CoRR abs\/","author":"Sutra Pierre","year":"1906"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2555243.2555260"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/79173.79181"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290372"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_20"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428278","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428278","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:57Z","timestamp":1750197777000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428278"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,13]]},"references-count":52,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2020,11,13]]}},"alternative-id":["10.1145\/3428278"],"URL":"https:\/\/doi.org\/10.1145\/3428278","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,11,13]]},"assertion":[{"value":"2020-11-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}