{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,4]],"date-time":"2025-04-04T23:04:18Z","timestamp":1743807858222,"version":"3.37.3"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2018,10,24]],"date-time":"2018-10-24T00:00:00Z","timestamp":1540339200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100010663","name":"European Research Council","doi-asserted-by":"publisher","award":["610150"],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001821","name":"Vienna Science and Technology Fund","doi-asserted-by":"publisher","award":["VRG11-005"],"id":[{"id":"10.13039\/501100001821","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["S11403-N23"],"id":[{"id":"10.13039\/501100002428","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":[[2018,10,24]]},"abstract":"\n Several recently proposed randomized testing tools for concurrent and distributed systems come with theoretical guarantees on their success. The key to these guarantees is a notion of bug depth\u2014the minimum length of a sequence of events sufficient to expose the bug\u2014and a characterization of\n d<\/jats:italic>\n -hitting families of schedules\u2014a set of schedules guaranteed to cover every bug of given depth\n d<\/jats:italic>\n . Previous results show that in certain cases the size of a\n d<\/jats:italic>\n -hitting family can be significantly smaller than the total number of possible schedules. However, these results either assume shared-memory multithreading, or that the underlying partial ordering of events is known statically and has special structure. These assumptions are not met by distributed message-passing applications.\n <\/jats:p>\n \n In this paper, we present a randomized scheduling algorithm for testing distributed systems. In contrast to previous approaches, our algorithm works for arbitrary partially ordered sets of events revealed online as the program is being executed. We show that for partial orders of width at most\n w<\/jats:italic>\n and size at most\n n<\/jats:italic>\n (both statically unknown), our algorithm is guaranteed to sample from at most\n w<\/jats:italic>\n 2<\/jats:sup>\n n<\/jats:italic>\n \n d<\/jats:italic>\n \u22121\n <\/jats:sup>\n schedules, for every fixed bug depth\n d<\/jats:italic>\n . Thus, our algorithm discovers a bug of depth\n d<\/jats:italic>\n with probability at least 1 \/ (\n w<\/jats:italic>\n 2<\/jats:sup>\n n<\/jats:italic>\n \n d<\/jats:italic>\n \u22121\n <\/jats:sup>\n ). As a special case, our algorithm recovers a previous randomized testing algorithm for multithreaded programs. Our algorithm is simple to implement, but the correctness arguments depend on difficult combinatorial results about online dimension and online chain partitioning of partially ordered sets.\n <\/jats:p>\n We have implemented our algorithm in a randomized testing tool for distributed message-passing programs. We show that our algorithm can find bugs in distributed systems such as Zookeeper and Cassandra, and empirically outperforms naive random exploration while providing theoretical guarantees.<\/jats:p>","DOI":"10.1145\/3276530","type":"journal-article","created":{"date-parts":[[2018,10,24]],"date-time":"2018-10-24T11:57:18Z","timestamp":1540382238000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":27,"title":["Randomized testing of distributed systems with probabilistic guarantees"],"prefix":"10.1145","volume":"2","author":[{"given":"Burcu Kulahcioglu","family":"Ozkan","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany"}]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]},{"given":"Filip","family":"Niksic","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]},{"given":"Mitra Tabaei","family":"Befrouei","sequence":"additional","affiliation":[{"name":"Vienna University of Technology, Austria"}]},{"given":"Georg","family":"Weissenbacher","sequence":"additional","affiliation":[{"name":"Vienna University of Technology, Austria"}]}],"member":"320","published-online":{"date-parts":[[2018,10,24]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535845"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-006-0004-y"},{"volume-title":"Retrieved","year":"2012","key":"e_1_2_2_3_1"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11083-011-9197-1"},{"key":"e_1_2_2_5_1","first-page":"P2","article-title":"An Easy Subexponential Bound for Online Chain Partitioning","volume":"25","author":"Bosek Bart\u0142omiej","year":"2018","journal-title":"Electr. J. Comb."},{"volume-title":"The Sub-exponential Upper Bound for On-Line Chain Partitioning. In 51th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2010","year":"2010","author":"Bosek Bart\u0142omiej","key":"e_1_2_2_6_1"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_31"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1736020.1736040"},{"key":"e_1_2_2_9_1","volume-title":"CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II (Lecture Notes in Computer Science)","volume":"9780","author":"Chistikov Dmitry","year":"2016"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737996"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/2930583.2930602"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786861"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.2307\/1969503"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2755573.2755601"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926432"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00204-6"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_2_2_18_1","unstructured":"Gatling Corp. 2011\u20132018. Gatling. Retrieved September 7 2018 from https:\/\/gatling.io\/ Gatling Corp. 2011\u20132018. Gatling. Retrieved September 7 2018 from https:\/\/gatling.io\/"},{"key":"e_1_2_2_19_1","unstructured":"Patrice Godefroid. 1996. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer-Verlag New York Inc. Secaucus NJ USA. Patrice Godefroid. 1996. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer-Verlag New York Inc. Secaucus NJ USA."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2011.5958223"},{"key":"e_1_2_2_21_1","first-page":"63","article-title":"An Effective Version of Dilworth\u2019s Theorem","volume":"268","author":"Kierstead Henry A.","year":"1981","journal-title":"Trans. Amer. Math. Soc."},{"key":"e_1_2_2_22_1","unstructured":"Kyle Kingsbury. 2013. Partitions for Everyone! Retrieved July 31 2018 from https:\/\/www.infoq.com\/presentations\/ partitioning- comparison Kyle Kingsbury. 2013. Partitions for Everyone! Retrieved July 31 2018 from https:\/\/www.infoq.com\/presentations\/ partitioning- comparison"},{"volume-title":"Jepsen. Retrieved","year":"2013","author":"Kingsbury Kyle","key":"e_1_2_2_23_1"},{"key":"e_1_2_2_24_1","first-page":"101","article-title":"Online dimension of partially ordered sets","volume":"42","author":"Kloch Kamil","year":"2007","journal-title":"Reports on Mathematical Logic"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1773912.1773922"},{"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","key":"e_1_2_2_26_1"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872374"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158134"},{"key":"e_1_2_2_29_1","doi-asserted-by":"crossref","unstructured":"Rashmi Mudduluru Pantazis Deligiannis Ankush Desai Akash Lal and Shaz Qadeer. 2017. Lasso Detection using PartialState Caching. https:\/\/www.microsoft.com\/en- us\/research\/publication\/lasso- detection- using- partial- state- caching- 2\/ Rashmi Mudduluru Pantazis Deligiannis Ankush Desai Akash Lal and Shaz Qadeer. 2017. Lasso Detection using PartialState Caching. https:\/\/www.microsoft.com\/en- us\/research\/publication\/lasso- detection- using- partial- state- caching- 2\/","DOI":"10.23919\/FMCAD.2017.8102245"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250785"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509538"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2013.6693072"},{"key":"e_1_2_2_34_1","volume-title":"CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II (Lecture Notes in Computer Science)","volume":"10982","author":"Yuan Xinhao","year":"2018"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3276530","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T10:28:26Z","timestamp":1672568906000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3276530"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10,24]]},"references-count":34,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2018,10,24]]}},"alternative-id":["10.1145\/3276530"],"URL":"https:\/\/doi.org\/10.1145\/3276530","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2018,10,24]]},"assertion":[{"value":"2018-10-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}