{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T08:59:57Z","timestamp":1775638797821,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":57,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,3,9]],"date-time":"2020-03-09T00:00:00Z","timestamp":1583712000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"JP Morgan","award":["Faculty Research Award"],"award-info":[{"award-number":["Faculty Research Award"]}]},{"DOI":"10.13039\/100008536","name":"Amazon Web Services","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100008536","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100007297","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-16-1- 2263,N00014-17-1-2788"],"award-info":[{"award-number":["N00014-16-1- 2263,N00014-17-1-2788"]}],"id":[{"id":"10.13039\/100007297","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006785","name":"Google","doi-asserted-by":"publisher","award":["Google Cloud grant"],"award-info":[{"award-number":["Google Cloud grant"]}],"id":[{"id":"10.13039\/100006785","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-15-64055"],"award-info":[{"award-number":["CNS-15-64055"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"DiDi","award":["Faculty Research Award"],"award-info":[{"award-number":["Faculty Research Award"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,3,9]]},"DOI":"10.1145\/3373376.3378484","type":"proceedings-article","created":{"date-parts":[[2020,3,13]],"date-time":"2020-03-13T22:37:01Z","timestamp":1584139021000},"page":"1141-1156","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":24,"title":["Effective Concurrency Testing for Distributed Systems"],"prefix":"10.1145","author":[{"given":"Xinhao","family":"Yuan","sequence":"first","affiliation":[{"name":"Columbia University, New York, NY, USA"}]},{"given":"Junfeng","family":"Yang","sequence":"additional","affiliation":[{"name":"Columbia University, New York, NY, USA"}]}],"member":"320","published-online":{"date-parts":[[2020,3,13]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Amazon simpledb. https:\/\/aws.amazon.com\/simpledb.  Amazon simpledb. https:\/\/aws.amazon.com\/simpledb."},{"key":"e_1_3_2_1_2_1","unstructured":"Apache cassandra. http:\/\/cassandra.apache.org.  Apache cassandra. http:\/\/cassandra.apache.org."},{"key":"e_1_3_2_1_3_1","unstructured":"Cassandra-6023. https:\/\/issues.apache.org\/jira\/browse\/CASSANDRA-6023.  Cassandra-6023. https:\/\/issues.apache.org\/jira\/browse\/CASSANDRA-6023."},{"key":"e_1_3_2_1_4_1","unstructured":"Erlang programming language. https:\/\/erlang.org.  Erlang programming language. https:\/\/erlang.org."},{"key":"e_1_3_2_1_5_1","unstructured":"The go programming language specification. https:\/\/golang.org\/ref\/spec.  The go programming language specification. https:\/\/golang.org\/ref\/spec."},{"key":"e_1_3_2_1_6_1","unstructured":"Why whatsapp only needs 50 engineers for its 900m users. https:\/\/www.wired.com\/2015\/09\/whatsapp-serves-900-million-users-50-engineers\/.  Why whatsapp only needs 50 engineers for its 900m users. https:\/\/www.wired.com\/2015\/09\/whatsapp-serves-900-million-users-50-engineers\/."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535845"},{"key":"e_1_3_2_1_8_1","first-page":"526","volume-title":"Miguel G\u00f3mez-Zamalloa, and Peter J. Stuckey. Context-sensitive dynamic partial order reduction. In Rupak Majumdar and Viktor Kunvc ak","author":"Albert Elvira","year":"2017","unstructured":"Elvira Albert , Puri Arenas , Mar\u00eda Garc\u00eda de la Banda , Miguel G\u00f3mez-Zamalloa, and Peter J. Stuckey. Context-sensitive dynamic partial order reduction. In Rupak Majumdar and Viktor Kunvc ak , editors, Computer Aided Verification, pages 526 -- 543 , Cham, 2017 . Springer International Publishing . Elvira Albert, Puri Arenas, Mar\u00eda Garc\u00eda de la Banda, Miguel G\u00f3mez-Zamalloa, and Peter J. Stuckey. Context-sensitive dynamic partial order reduction. In Rupak Majumdar and Viktor Kunvc ak, editors, Computer Aided Verification, pages 526--543, Cham, 2017. Springer International Publishing."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/3291168.3291173"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66845-1_15"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89963-3_14"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2168836.2168865"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1736020.1736040"},{"key":"e_1_3_2_1_14_1","volume-title":"Core erlang 1.0.3 language specification","author":"Carlsson Richard","year":"2004","unstructured":"Richard Carlsson , Bj\u00f6rn Gustavsson , Erik Johansson , Thomas Lindgren , Sven-Olof Nystr\u00f6m , Mikael Pettersson , and Robert Virding . Core erlang 1.0.3 language specification . 2004 . Richard Carlsson, Bj\u00f6rn Gustavsson, Erik Johansson, Thomas Lindgren, Sven-Olof Nystr\u00f6m, Mikael Pettersson, and Robert Virding. Core erlang 1.0.3 language specification. 2004."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2013.50"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596574"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737996"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542490"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291171"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/547238"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043582"},{"key":"e_1_3_2_1_24_1","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"Jackson Daniel","year":"2006","unstructured":"Daniel Jackson . Software Abstractions: Logic, Language, and Analysis . The MIT Press , 2006 . Daniel Jackson. Software Abstractions: Logic, Language, and Analysis. The MIT Press, 2006."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250755"},{"key":"e_1_3_2_1_26_1","first-page":"2019","author":"Kingsbury Kyle","year":"2016","unstructured":"Kyle Kingsbury . Jepsen , 2016 -- 2019 . Kyle Kingsbury. Jepsen, 2016--2019.","journal-title":"Jepsen"},{"key":"e_1_3_2_1_27_1","first-page":"399","volume-title":"Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation, OSDI'14","author":"Leesatapornwongsa Tanakorn","year":"2014","unstructured":"Tanakorn Leesatapornwongsa , Mingzhe Hao , Pallavi Joshi , Jeffrey F. Lukman , and Haryadi S. Gunawi . Samc: Semantic-aware model checking for fast discovery of deep bugs in cloud systems . In Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation, OSDI'14 , pages 399 -- 414 , Berkeley, CA, USA , 2014 . USENIX Association. Tanakorn Leesatapornwongsa, Mingzhe Hao, Pallavi Joshi, Jeffrey F. Lukman, and Haryadi S. Gunawi. Samc: Semantic-aware model checking for fast discovery of deep bugs in cloud systems. In Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation, OSDI'14, pages 399--414, Berkeley, CA, USA, 2014. USENIX Association."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872374"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3037697.3037735"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3173162.3177161"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168864"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3302424.3303986"},{"key":"e_1_3_2_1_33_1","volume-title":"Proc. ACM Program. Lang., 2(POPL):46:1--46:24","author":"Majumdar Rupak","year":"2017","unstructured":"Rupak Majumdar and Filip Niksic . Why is random testing effective for partition tolerance bugs? Proc. ACM Program. Lang., 2(POPL):46:1--46:24 , December 2017 . Rupak Majumdar and Filip Niksic. Why is random testing effective for partition tolerance bugs? Proc. ACM Program. Lang., 2(POPL):46:1--46:24, December 2017."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2146382.2146391"},{"key":"e_1_3_2_1_35_1","first-page":"215","volume-title":"Parallel and Distributed Algorithms","author":"Mattern Friedemann","year":"1989","unstructured":"Friedemann Mattern . Virtual time and global states of distributed systems . Parallel and Distributed Algorithms , pages 215 -- 226 , 1989 . Friedemann Mattern. Virtual time and global states of distributed systems. Parallel and Distributed Algorithms, pages 215--226, 1989."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1060289.1060297"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250785"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/1855741.1855760"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134018"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/781498.781528"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/2643634.2643666"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276530"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360606"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1508244.1508249"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1321631.1321679"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375584"},{"key":"e_1_3_2_1_47_1","first-page":"3","volume-title":"Proceedings of the 5th International Conference on Systems Software Verification, SSV'10","author":"Simsa Jiri","year":"2010","unstructured":"Jiri Simsa , Randy Bryant , and Garth Gibson . dbug : Systematic evaluation of distributed systems . In Proceedings of the 5th International Conference on Systems Software Verification, SSV'10 , pages 3 -- 3 , Berkeley, CA, USA , 2010 . USENIX Association. Jiri Simsa, Randy Bryant, and Garth Gibson. dbug: Systematic evaluation of distributed systems. In Proceedings of the 5th International Conference on Systems Software Verification, SSV'10, pages 3--3, Berkeley, CA, USA, 2010. USENIX Association."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2858651"},{"key":"e_1_3_2_1_49_1","first-page":"7","volume-title":"Proceedings of the 6th Conference on Symposium on Opearting Systems Design & Implementation -","volume":"6","author":"van Renesse Robbert","year":"2004","unstructured":"Robbert van Renesse and Fred B. Schneider . Chain replication for supporting high throughput and availability . In Proceedings of the 6th Conference on Symposium on Opearting Systems Design & Implementation - Volume 6 , OSDI'04, pages 7 -- 7 , Berkeley, CA, USA , 2004 . USENIX Association. Robbert van Renesse and Fred B. Schneider. Chain replication for supporting high throughput and availability. In Proceedings of the 6th Conference on Symposium on Opearting Systems Design & Implementation - Volume 6, OSDI'04, pages 7--7, Berkeley, CA, USA, 2004. USENIX Association."},{"key":"e_1_3_2_1_50_1","first-page":"205","volume-title":"Proceedings of the the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering, ESEC-FSE '07","author":"Voung Jan Wen","year":"2007","unstructured":"Jan Wen Voung , Ranjit Jhala , and Sorin Lerner . Relay : Static race detection on millions of lines of code . In Proceedings of the the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering, ESEC-FSE '07 , pages 205 -- 214 , New York, NY, USA , 2007 . ACM. Jan Wen Voung, Ranjit Jhala, and Sorin Lerner. Relay: Static race detection on millions of lines of code. In Proceedings of the the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering, ESEC-FSE '07, pages 205--214, New York, NY, USA, 2007. ACM."},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985824"},{"key":"e_1_3_2_1_52_1","volume-title":"Github - locks","author":"Wiger Ulf","year":"2017","unstructured":"Ulf Wiger . Github - locks , 2017 . Ulf Wiger. Github - locks, 2017."},{"key":"e_1_3_2_1_53_1","first-page":"213","volume-title":"Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation, NSDI'09","author":"Yang Junfeng","year":"2009","unstructured":"Junfeng Yang , Tisheng Chen , Ming Wu , Zhilei Xu , Xuezheng Liu , Haoxiang Lin , Mao Yang , Fan Long , Lintao Zhang , and Lidong Zhou . Modist : Transparent model checking of unmodified distributed systems . In Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation, NSDI'09 , pages 213 -- 228 , Berkeley, CA, USA , 2009 . USENIX Association. Junfeng Yang, Tisheng Chen, Ming Wu, Zhilei Xu, Xuezheng Liu, Haoxiang Lin, Mao Yang, Fan Long, Lintao Zhang, and Lidong Zhou. Modist: Transparent model checking of unmodified distributed systems. In Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation, NSDI'09, pages 213--228, Berkeley, CA, USA, 2009. USENIX Association."},{"key":"e_1_3_2_1_54_1","first-page":"10","volume-title":"Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation -","volume":"7","author":"Yang Junfeng","year":"2006","unstructured":"Junfeng Yang , Can Sar , and Dawson Engler . Explode : A lightweight, general system for finding serious storage system errors . In Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation - Volume 7 , OSDI '06, pages 10 -- 10 , Berkeley, CA, USA , 2006 . USENIX Association. Junfeng Yang, Can Sar, and Dawson Engler. Explode: A lightweight, general system for finding serious storage system errors. In Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation - Volume 7, OSDI '06, pages 10--10, Berkeley, CA, USA, 2006. USENIX Association."},{"key":"e_1_3_2_1_55_1","first-page":"19","volume-title":"Proceedings of the 6th Conference on Symposium on Opearting Systems Design & Implementation -","volume":"6","author":"Yang Junfeng","year":"2004","unstructured":"Junfeng Yang , Paul Twohey , Dawson Engler , and Madanlal Musuvathi . Using model checking to find serious file system errors . In Proceedings of the 6th Conference on Symposium on Opearting Systems Design & Implementation - Volume 6 , OSDI'04, pages 19 -- 19 , Berkeley, CA, USA , 2004 . USENIX Association. Junfeng Yang, Paul Twohey, Dawson Engler, and Madanlal Musuvathi. Using model checking to find serious file system errors. In Proceedings of the 6th Conference on Symposium on Opearting Systems Design & Implementation - Volume 6, OSDI'04, pages 19--19, Berkeley, CA, USA, 2004. USENIX Association."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384651"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_20"}],"event":{"name":"ASPLOS '20: Architectural Support for Programming Languages and Operating Systems","location":"Lausanne Switzerland","acronym":"ASPLOS '20","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGOPS ACM Special Interest Group on Operating Systems","SIGARCH ACM Special Interest Group on Computer Architecture","SIGBED ACM Special Interest Group on Embedded Systems"]},"container-title":["Proceedings of the Twenty-Fifth International Conference on Architectural Support for Programming Languages and Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3373376.3378484","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/abs\/10.1145\/3373376.3378484","content-type":"text\/html","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3373376.3378484","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3373376.3378484","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:32:59Z","timestamp":1750199579000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3373376.3378484"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,3,9]]},"references-count":57,"alternative-id":["10.1145\/3373376.3378484","10.1145\/3373376"],"URL":"https:\/\/doi.org\/10.1145\/3373376.3378484","relation":{},"subject":[],"published":{"date-parts":[[2020,3,9]]},"assertion":[{"value":"2020-03-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}