{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:38Z","timestamp":1772164058457,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":52,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,4,4]],"date-time":"2017-04-04T00:00:00Z","timestamp":1491264000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000144","name":"Division of Computer and Network Systems","doi-asserted-by":"publisher","award":["1563956, 1514256"],"award-info":[{"award-number":["1563956, 1514256"]}],"id":[{"id":"10.13039\/100000144","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["1514189, 1439091"],"award-info":[{"award-number":["1514189, 1439091"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]},{"name":"CERES research center"},{"DOI":"10.13039\/100000879","name":"Alfred P. Sloan Foundation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000879","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Google Faculty Research Award"},{"DOI":"10.13039\/100000145","name":"Division of Information and Intelligent Systems","doi-asserted-by":"publisher","award":["1546543"],"award-info":[{"award-number":["1546543"]}],"id":[{"id":"10.13039\/100000145","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003816","name":"Huawei Technologies","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100003816","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,4,4]]},"DOI":"10.1145\/3037697.3037735","type":"proceedings-article","created":{"date-parts":[[2017,4,5]],"date-time":"2017-04-05T08:47:40Z","timestamp":1491382060000},"page":"677-691","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":31,"title":["DCatch"],"prefix":"10.1145","author":[{"given":"Haopeng","family":"Liu","sequence":"first","affiliation":[{"name":"University of Chicago, Chicago, USA"}]},{"given":"Guangpu","family":"Li","sequence":"additional","affiliation":[{"name":"University of Chicago, Chicago, USA"}]},{"given":"Jeffrey F.","family":"Lukman","sequence":"additional","affiliation":[{"name":"University of Chicago, Chicago, USA"}]},{"given":"Jiaxin","family":"Li","sequence":"additional","affiliation":[{"name":"University of Chicago, Chicago, USA"}]},{"given":"Shan","family":"Lu","sequence":"additional","affiliation":[{"name":"University of Chicago, Chicago, USA"}]},{"given":"Haryadi S.","family":"Gunawi","sequence":"additional","affiliation":[{"name":"University of Chicago, Chicago, USA"}]},{"given":"Chen","family":"Tian","sequence":"additional","affiliation":[{"name":"Huawei US R&D Center, Sanfrancisco, USA"}]}],"member":"320","published-online":{"date-parts":[[2017,4,4]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions","author":"Bertot Yves","year":"2004","unstructured":"Yves Bertot and Pierre Cast\u00e9ran . Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions . Springer , 2004 . http:\/\/www.labri.fr\/perso\/casteran\/CoqArt\/index.html. Yves Bertot and Pierre Cast\u00e9ran. Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Springer, 2004. http:\/\/www.labri.fr\/perso\/casteran\/CoqArt\/index.html."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009895"},{"key":"e_1_3_2_1_3_1","volume-title":"OSDI","author":"Burrows Mike","year":"2006","unstructured":"Mike Burrows . The Chubby lock service for loosely-coupled distributed systems . In OSDI , 2006 . Mike Burrows. The Chubby lock service for loosely-coupled distributed systems. In OSDI, 2006."},{"key":"e_1_3_2_1_4_1","volume-title":"OSDI","author":"Chang Fay","year":"2006","unstructured":"Fay Chang , Jeffrey Dean , Sanjay Ghemawat , Wilson C. Hsieh , Deborah A. Wallach , Michael Burrows , Tushar Chandra , Andrew Fikes , and Robert Gruber . Bigtable : A Distributed Storage System for Structured Data . In OSDI , 2006 . Fay Chang, Jeffrey Dean, Sanjay Ghemawat, Wilson C. Hsieh, Deborah A. Wallach, Michael Burrows, Tushar Chandra, Andrew Fikes, and Robert Gruber. Bigtable: A Distributed Storage System for Structured Data. In OSDI, 2006."},{"key":"e_1_3_2_1_5_1","volume-title":"OSDI","author":"Dean Jeffrey","year":"2004","unstructured":"Jeffrey Dean and Sanjay Ghemawat . MapReduce : Simplified Data Processing on Large Clusters . In OSDI , 2004 . Jeffrey Dean and Sanjay Ghemawat. MapReduce: Simplified Data Processing on Large Clusters. In OSDI, 2004."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1294261.1294281"},{"key":"e_1_3_2_1_7_1","volume-title":"PLDI","author":"Desai Ankush","year":"2013","unstructured":"Ankush Desai , Vivek Gupta , Ethan Jackson , Shaz Qadeer , Sriram Rajamani , and Damien Zufferey . P : Safe Asynchronous Event-Driven Programming . In PLDI , 2013 . Ankush Desai, Vivek Gupta, Ethan Jackson, Shaz Qadeer, Sriram Rajamani, and Damien Zufferey. P: Safe Asynchronous Event-Driven Programming. In PLDI, 2013."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/982962.964023"},{"key":"e_1_3_2_1_9_1","volume-title":"FastTrack: Efficient and Precise Dynamic Race Detection. In PLDI","author":"Flanagan Cormac","year":"2009","unstructured":"Cormac Flanagan and Stephen N . Freund . FastTrack: Efficient and Precise Dynamic Race Detection. In PLDI , 2009 . Cormac Flanagan and Stephen N. Freund. FastTrack: Efficient and Precise Dynamic Race Detection. In PLDI, 2009."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1950365.1950394"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/945445.945450"},{"key":"e_1_3_2_1_12_1","volume-title":"NSDI","author":"Gunawi Haryadi S.","year":"2011","unstructured":"Haryadi S. Gunawi , Thanh Do , Pallavi Joshi , Peter Alvaro , Joseph M. Hellerstein , Andrea C. Arpaci-Dusseau , Remzi H. Arpaci-Dusseau , Koushik Sen , and Dhruba Borthakur .textsc Fate andtextsc Destini : A Framework for Cloud Recovery Testing . In NSDI , 2011 . Haryadi S. Gunawi, Thanh Do, Pallavi Joshi, Peter Alvaro, Joseph M. Hellerstein, Andrea C. Arpaci-Dusseau, Remzi H. Arpaci-Dusseau, Koushik Sen, and Dhruba Borthakur.textscFate andtextscDestini: A Framework for Cloud Recovery Testing. In NSDI, 2011."},{"key":"e_1_3_2_1_13_1","unstructured":"Haryadi S. Gunawi Mingzhe Hao Tanakorn Leesatapornwongsa Tiratat Patana-anake Thanh Do Jeffry Adityatama Kurnia J. Eliazar Agung Laksono Jeffrey F. Lukman Vincentius Martin and Anang D. Satria. What Bugs Live in the Cloud? A Study of 3000  Haryadi S. Gunawi Mingzhe Hao Tanakorn Leesatapornwongsa Tiratat Patana-anake Thanh Do Jeffry Adityatama Kurnia J. Eliazar Agung Laksono Jeffrey F. Lukman Vincentius Martin and Anang D. Satria. What Bugs Live in the Cloud? A Study of 3000"},{"key":"e_1_3_2_1_14_1","volume-title":"SoCC","author":"Cloud Systems Issues","year":"2014","unstructured":"Issues in Cloud Systems . In SoCC , 2014 . Issues in Cloud Systems. In SoCC, 2014."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043582"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_17_1","volume-title":"NSDI","author":"Hindman Benjamin","year":"2011","unstructured":"Benjamin Hindman , Andy Konwinski , Matei Zaharia , Ali Ghodsi , Anthony D. Joseph , Randy Katz , Scott Shenker , and Ion Stoica . Mesos : A Platform for Fine-Grained Resource Sharing in the Data Center . In NSDI , 2011 . Benjamin Hindman, Andy Konwinski, Matei Zaharia, Ali Ghodsi, Anthony D. Joseph, Randy Katz, Scott Shenker, and Ion Stoica. Mesos: A Platform for Fine-Grained Resource Sharing in the Data Center. In NSDI, 2011."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594330"},{"key":"e_1_3_2_1_19_1","volume-title":"ATC","author":"Hunt Patrick","year":"2010","unstructured":"Patrick Hunt , Mahadev Konar , Flavio P. Junqueira , and Benjamin Reed . ZooKeeper : Wait-free coordination for Internet-scale systems . In ATC , 2010 . Patrick Hunt, Mahadev Konar, Flavio P. Junqueira, and Benjamin Reed. ZooKeeper: Wait-free coordination for Internet-scale systems. In ATC, 2010."},{"key":"e_1_3_2_1_20_1","volume-title":"Data Race Bugs: Telling the Difference with Portend. In ASPLOS","author":"Kasikci Baris","year":"2012","unstructured":"Baris Kasikci , Cristian Zamfir , and George Candea . Data Races vs . Data Race Bugs: Telling the Difference with Portend. In ASPLOS , 2012 . Baris Kasikci, Cristian Zamfir, and George Candea. Data Races vs. Data Race Bugs: Telling the Difference with Portend. In ASPLOS, 2012."},{"key":"e_1_3_2_1_21_1","volume-title":"NSDI","author":"Killian Charles","year":"2007","unstructured":"Charles Killian , James Anderson , Ranjit Jhala , and Amin Vahdat . Life, Death, and the Critical Transition : Finding Liveness Bugs in Systems Code . In NSDI , 2007 . Charles Killian, James Anderson, Ranjit Jhala, and Amin Vahdat. Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code. In NSDI, 2007."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_3_2_1_23_1","unstructured":"Leslie Lamport. Specifying Systems: The TLA  Leslie Lamport. Specifying Systems: The TLA"},{"key":"e_1_3_2_1_24_1","volume-title":"Inc.","author":"Hardware Language","year":"2002","unstructured":"Language and Tools for Hardware and Software Engineers . Addison-Wesley Longman Publishing Co ., Inc. , Boston, MA, USA , 2002 . Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 2002."},{"key":"e_1_3_2_1_25_1","volume-title":"SAMC: Semantic-Aware Model Checking for Fast Discovery of Deep Bugs in Cloud Systems. In OSDI","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 OSDI , 2014 . 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 OSDI, 2014."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872374"},{"key":"e_1_3_2_1_27_1","volume-title":"NSDI","author":"Liu Xuezheng","year":"2007","unstructured":"Xuezheng Liu , Wei Lin , Aimin Pan , and Zheng Zhang . Wi DS Checker : Combating Bugs in Distributed Systems . In NSDI , 2007 . Xuezheng Liu, Wei Lin, Aimin Pan, and Zheng Zhang. WiDS Checker: Combating Bugs in Distributed Systems. In NSDI, 2007."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168864"},{"key":"e_1_3_2_1_29_1","volume-title":"ISCA","author":"Lucia Brandon","year":"2010","unstructured":"Brandon Lucia , Luis Ceze , and Karin Strauss . ColorSafe : Architectural Support for Debugging and Dynamically Avoiding Multi-Variable Atomicity Violations . In ISCA , 2010 . Brandon Lucia, Luis Ceze, and Karin Strauss. ColorSafe: Architectural Support for Debugging and Dynamically Avoiding Multi-Variable Atomicity Violations. In ISCA, 2010."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815415"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594311"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2522738"},{"key":"e_1_3_2_1_33_1","volume-title":"OSDI","author":"Musuvathi Madanlal","year":"2008","unstructured":"Madanlal Musuvathi , Shaz Qadeer , Thomas Ball , Gerard Basler , Piramanayagam Arumuga Nainar , and Iulian Neamtiu . Finding and Reproducing Heisenbugs in Concurrent Programs . In OSDI , 2008 . Madanlal Musuvathi, Shaz Qadeer, Thomas Ball, Gerard Basler, Piramanayagam Arumuga Nainar, and Iulian Neamtiu. Finding and Reproducing Heisenbugs in Concurrent Programs. In OSDI, 2008."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/109625.109640"},{"key":"e_1_3_2_1_35_1","volume-title":"OSDI","author":"Nightingale Edmund B.","year":"2012","unstructured":"Edmund B. Nightingale , Jeremy Elson , Jinliang Fan , Owen Hofmann , Jon Howell , and Yutaka Suzue . Flat Datacenter Storage . In OSDI , 2012 . Edmund B. Nightingale, Jeremy Elson, Jinliang Fan, Owen Hofmann, Jon Howell, and Yutaka Suzue. Flat Datacenter Storage. In OSDI, 2012."},{"key":"e_1_3_2_1_36_1","volume-title":"ATC","author":"Ongaro Diego","year":"2014","unstructured":"Diego Ongaro and John Ousterhout . In Search of an Understandable Consensus Algorithm . In ATC , 2014 . Diego Ongaro and John Ousterhout. In Search of an Understandable Consensus Algorithm. In ATC, 2014."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1508244.1508249"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509538"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/268998.266641"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375584"},{"key":"e_1_3_2_1_41_1","volume-title":"OOPSLA","author":"Shi Yao","year":"2010","unstructured":"Yao Shi , Soyeon Park , Zuoning Yin , Shan Lu , Yuanyuan Zhou , Wenguang Chen , and Weimin Zheng . Do I Use the Wrong Definition? DefUse : Definition-Use Invariants for Detecting Concurrency and Sequential Bugs . In OOPSLA , 2010 . Yao Shi, Soyeon Park, Zuoning Yin, Shan Lu, Yuanyuan Zhou, Wenguang Chen, and Weimin Zheng. Do I Use the Wrong Definition? DefUse: Definition-Use Invariants for Detecting Concurrency and Sequential Bugs. In OOPSLA, 2010."},{"key":"e_1_3_2_1_42_1","volume-title":"Mike Burrows, Pat Stephenson, Manoj Plakal, Donald Beaver, Saul Jaspan, and Chandan Shanbhag. Dapper, a Large-Scale Distributed Systems Tracing Infrastructure. Technical report, Google","author":"Sigelman Benjamin H.","year":"2010","unstructured":"Benjamin H. Sigelman , Luiz Andr\u00e9 Barroso , Mike Burrows, Pat Stephenson, Manoj Plakal, Donald Beaver, Saul Jaspan, and Chandan Shanbhag. Dapper, a Large-Scale Distributed Systems Tracing Infrastructure. Technical report, Google , Inc ., 2010 . Benjamin H. Sigelman, Luiz Andr\u00e9 Barroso, Mike Burrows, Pat Stephenson, Manoj Plakal, Donald Beaver, Saul Jaspan, and Chandan Shanbhag. Dapper, a Large-Scale Distributed Systems Tracing Infrastructure. Technical report, Google, Inc., 2010."},{"key":"e_1_3_2_1_43_1","volume-title":"SSV","author":"Simsa Jiri","year":"2010","unstructured":"Jiri Simsa , Randy Bryant , and Garth Gibson . dBug : Systematic Evaluation of Distributed Systems . In SSV , 2010 . Jiri Simsa, Randy Bryant, and Garth Gibson. dBug: Systematic Evaluation of Distributed Systems. In SSV, 2010."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390649"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2523616.2523633"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043590"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_3_2_1_48_1","volume-title":"OSDI","author":"Xiong Weiwei","year":"2010","unstructured":"Weiwei Xiong , Soyeon Park , Jiaqi Zhang , Yuanyuan Zhou , and Zhiqiang Ma . Ad Hoc Synchronization Considered Harmful . In OSDI , 2010 . Weiwei Xiong, Soyeon Park, Jiaqi Zhang, Yuanyuan Zhou, and Zhiqiang Ma. Ad Hoc Synchronization Considered Harmful. In OSDI, 2010."},{"key":"e_1_3_2_1_49_1","volume-title":"NSDI","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 NSDI , 2009 . 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 NSDI, 2009."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2155620.2155645"},{"key":"e_1_3_2_1_51_1","volume-title":"ASPLOS","author":"Zhang Wei","year":"2011","unstructured":"Wei Zhang , Junghee Lim , Ramya Olichandran , Joel Scherpelz , Guoliang Jin , Shan Lu , and Thomas Reps . ConSeq : Detecting Concurrency Bugs through Sequential Errors . In ASPLOS , 2011 . Wei Zhang, Junghee Lim, Ramya Olichandran, Joel Scherpelz, Guoliang Jin, Shan Lu, and Thomas Reps. ConSeq: Detecting Concurrency Bugs through Sequential Errors. In ASPLOS, 2011."},{"key":"e_1_3_2_1_52_1","volume-title":"ASPLOS","author":"Zhang Wei","year":"2010","unstructured":"Wei Zhang , Chong Sun , and Shan Lu. ConMem : Detecting Severe Concurrency Bugs through an Effect-Oriented Approach . In ASPLOS , 2010 . Wei Zhang, Chong Sun, and Shan Lu. ConMem: Detecting Severe Concurrency Bugs through an Effect-Oriented Approach. In ASPLOS, 2010."}],"event":{"name":"ASPLOS '17: Architectural Support for Programming Languages and Operating Systems","location":"Xi'an China","acronym":"ASPLOS '17","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-Second International Conference on Architectural Support for Programming Languages and Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3037697.3037735","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3037697.3037735","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3037697.3037735","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:03:10Z","timestamp":1750201390000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3037697.3037735"}},"subtitle":["Automatically Detecting Distributed Concurrency Bugs in Cloud Systems"],"short-title":[],"issued":{"date-parts":[[2017,4,4]]},"references-count":52,"alternative-id":["10.1145\/3037697.3037735","10.1145\/3037697"],"URL":"https:\/\/doi.org\/10.1145\/3037697.3037735","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3093336.3037735","asserted-by":"object"},{"id-type":"doi","id":"10.1145\/3093337.3037735","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2017,4,4]]},"assertion":[{"value":"2017-04-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}