{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T17:25:52Z","timestamp":1787592352579,"version":"build-2736575974"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1815496"],"award-info":[{"award-number":["1815496"]}],"id":[{"id":"10.13039\/100000001","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":[[2025,4,9]]},"abstract":"<jats:p>A predictive analysis takes an execution trace as input and discovers concurrency bugs without accessing the program source code. A sound predictive analysis reports no false positives, which sounds like a property that can be defined easily, but which has been defined in many different ways in previous work. In this paper, we unify, simplify, and generalize those soundness defInitions for analyses that discover concurrency bugs that can be represented as a consecutive sequence of events. Our soundness defInition is graph based, separates thread-local properties and whole-execution properties, and works well with weak memory executions. We also present a three-step proof recipe, and we use it to prove six existing analyses sound. This includes the first proof of soundness for a predictive analysis that works with weak memory.<\/jats:p>","DOI":"10.1145\/3720435","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"590-616","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Soundness of Predictive Concurrency Analyses"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1601-9086","authenticated-orcid":false,"given":"Shuyang","family":"Liu","sequence":"first","affiliation":[{"name":"University of California at Los Angeles, Computer Science, Los Angeles, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6068-7866","authenticated-orcid":false,"given":"Doug","family":"Lea","sequence":"additional","affiliation":[{"name":"SUNY Oswego, Computer Science, Oswego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4747-365X","authenticated-orcid":false,"given":"Jens","family":"Palsberg","sequence":"additional","affiliation":[{"name":"University of California at Los Angeles, Computer Science, Los Angeles, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3458926"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/1481839.1481842"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0135-z"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3468264.3468549"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/1543135.1542490"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3360605"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","unstructured":"Jeff Huang Qingzhou Luo and Grigore Rosu. 2015. GPredict: Generic Predictive Concurrency Analysis. 2015 IEEE\/ACM 37th IEEE International Conference on Software Engineering 1 (5 2015) 847\u2013857. doi:10.1109\/ICSE.2015.96","DOI":"10.1109\/ICSE.2015.96"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594315"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984025"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/3276516"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062374"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571212"},{"key":"e_1_3_1_14_2","volume-title":"arXiv preprint arXiv:2012.01067","author":"Lahav Ori","year":"2020","unstructured":"Ori Lahav, Egor Namakonov, Jonas Oberhauser, Anton Podkopaev, and Viktor Vafeiadis. 2020. Making Weak Memory Models Fair. arXiv preprint arXiv:2012.01067 (12 2020). http:\/\/arxiv.org\/abs\/2012.01067"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591253"},{"key":"e_1_3_1_17_2","unstructured":"Luc Maranget Susmit Sarkar and Peter Sewell. 2012. A Tutorial Introduction to the ARM and POWER Relaxed Memory Models. 50 pages. https:\/\/www.cl.cam.ac.uk\/~pes20\/ppc-supplemental\/test7.pdf Draft available from http:\/\/www. cl. cam. ac. uk\/ pes20\/ppc-supplemental\/test7.pdf."},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3276515"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434317"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371085"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290382"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158107"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","unstructured":"Susmit Sarkar Peter Sewell Jade Alglave Luc Maranget and Derek Williams. 2011. Understanding POWER multiprocessors. Proceedings of the 32nd ACM SIGPLAN conference on Programming language design and implementation - PLDI \u201911 175. doi:10.1145\/1993498.1993520","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35632-2_16"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3597503.3639099"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/2103621.2103702"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591291"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720435","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720435","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720435","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T16:31:19Z","timestamp":1787589079000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720435"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":27,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720435"],"URL":"https:\/\/doi.org\/10.1145\/3720435","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}