{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T11:35:01Z","timestamp":1791459301401,"version":"4.3.4"},"reference-count":38,"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":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,10,24]]},"abstract":"<jats:p>For a concurrent program, a prediction tool maps the history of a single run to a prediction of bugs in an exponential number of other runs. If all those bugs can occur, then the tool is sound. This is the case for some data race tools like RVPredict, but was, until now, not the case for deadlock tools. We present the first sound tool for predicting deadlocks in Java. Unlike previous work, we use request events and a novel form of executability constraints that enable sound and effective deadlock prediction. We model prediction as a general decision problem, which we show is decidable and can be instantiated to both deadlocks and data races. Our proof of decidability maps the decision problem to an equivalent constraint problem that we solve using an SMT-solver. Our experiments show that our tool finds real deadlocks effectively, including some missed by DeadlockFuzzer, which verifies each deadlock candidate by re-executing the input program. Our experiments also show that our tool can be used to predict more, real data races than RVPredict.<\/jats:p>","DOI":"10.1145\/3276516","type":"journal-article","created":{"date-parts":[[2018,10,24]],"date-time":"2018-10-24T11:57:18Z","timestamp":1540382238000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":37,"title":["Sound deadlock prediction"],"prefix":"10.1145","volume":"2","author":[{"given":"Christian Gram","family":"Kalhauge","sequence":"first","affiliation":[{"name":"University of California at Los Angeles, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jens","family":"Palsberg","sequence":"additional","affiliation":[{"name":"University of California at Los Angeles, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2018,10,24]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11678779_15"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1167515.1167488"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985827"},{"key":"e_1_2_2_4_1","unstructured":"Eric Bruneton Romain Lenglet and Thierry Coupaye. 2002. ASM: a code manipulation tool to implement adaptable systems. Adaptable and extensible component systems 30 19 (2002).  Eric Bruneton Romain Lenglet and Thierry Coupaye. 2002. ASM: a code manipulation tool to implement adaptable systems. Adaptable and extensible component systems 30 19 (2002)."},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/2337223.2337294"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2014.2301725"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2014.2307864"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2016.2537335"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568312"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368119"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2011.22"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1097-024X(199906)29:7%3C577::AID-SPE246%3E3.0.CO;2-V"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-005-3861-2"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411203.1411255"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_5"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181787"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1165389.945468"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2635868.2635918"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/645880.672080"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/645880.672085"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050043"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0169-7552(93)90095-L"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737975"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/2818754.2818856"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594315"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1543135.1542489"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062374"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2015.87"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2009.5070538"},{"key":"e_1_2_2_32_1","doi-asserted-by":"crossref","unstructured":"Mahmoud Said Chao Wang Zijiang Yang Karem Sakallah and Karem Sakallahg. 2011. Generating data race witnesses by an SMT-based analysis. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 6617 LNCS (2011) 313\u2013327.   Mahmoud Said Chao Wang Zijiang Yang Karem Sakallah and Karem Sakallahg. 2011. Generating data race witnesses by an SMT-based analysis. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 6617 LNCS (2011) 313\u2013327.","DOI":"10.1007\/978-3-642-20398-5_23"},{"key":"e_1_2_2_34_1","volume-title":"International Conference on Runtime Verification. Springer, 136\u2013150","author":"\u015eerb\u0103nu\u0163\u0103 Traian Florin","year":"2012"},{"key":"e_1_2_2_35_1","volume-title":"International Conference on Runtime Verification. Springer, 136\u2013150","author":"Serbanuta Traian Florin","year":"2012"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103621.2103702"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23404-5_13"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022920129859"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_17"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3276516","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3276516","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:03:39Z","timestamp":1750273419000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3276516"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10,24]]},"references-count":38,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2018,10,24]]}},"alternative-id":["10.1145\/3276516"],"URL":"https:\/\/doi.org\/10.1145\/3276516","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"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"}}]}}