{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T23:06:58Z","timestamp":1768259218406,"version":"3.49.0"},"reference-count":93,"publisher":"Association for Computing Machinery (ACM)","issue":"3","funder":[{"name":"European Union and the Sponsor Estonian Research Council","award":["#PRG2764 and #TEM-TA119"],"award-info":[{"award-number":["#PRG2764 and #TEM-TA119"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2025,9,30]]},"abstract":"<jats:p>Sound static data race freedom verification has been a long-standing challenge in the field of programming languages. While actively researched a decade ago, most practical data race detection tools have since abandoned soundness. Is sound static race freedom verification for real-world C programs a lost cause? In this work, we investigate the obstacles to making significant progress in automated race freedom verification. We selected a benchmark suite of real-world programs and, as our primary contribution, extracted a set of coding idioms that represent fundamental barriers to verification. We expressed these idioms as micro-benchmarks and contributed them as evaluation tasks for the International Competition on Software Verification, SV-COMP. To understand the current state, we measure how sound automated verification tools competing in SV-COMP perform on these idioms and also when used out of the box on the real-world programs. For 8 of the 20 coding idioms, there does exist an automated race freedom verifier that can verify it; however, we also found significant unsoundness in leading verifiers, including Goblint and Deagle. Five of the seven tools failed to return any result on any real-world benchmarks under our chosen resource limitations, with the remaining two tools verifying race freedom for 2 of the 18 programs and crashing or returning inconclusive results on the others. We thus show that state-of-the-art verifiers have both superficial and fundamental barriers to correctly analyzing real-world programs. These barriers constitute the open problems that must be solved to make progress on automated static data race freedom verification.<\/jats:p>","DOI":"10.1145\/3732933","type":"journal-article","created":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T11:36:17Z","timestamp":1745926577000},"page":"1-40","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Sound Static Data Race Verification for C: Is the Race Lost?"],"prefix":"10.1145","volume":"47","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-3725-4131","authenticated-orcid":false,"given":"Karoliine","family":"Holter","sequence":"first","affiliation":[{"name":"University of Tartu, Tartu, Estonia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4553-1350","authenticated-orcid":false,"given":"Simmo","family":"Saan","sequence":"additional","affiliation":[{"name":"University of Tartu, Tartu, Estonia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8278-5400","authenticated-orcid":false,"given":"Patrick","family":"Lam","sequence":"additional","affiliation":[{"name":"University of Waterloo, Ontario, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4336-7980","authenticated-orcid":false,"given":"Vesal","family":"Vojdani","sequence":"additional","affiliation":[{"name":"University of Tartu, Tartu, Estonia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,9,15]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99527-0_34"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48288-9_5"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24372-1_3"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35182-2_12"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_3_3_7_2","first-page":"470","volume-title":"Proceedings of the 2016 IEEE 23rd International Conference on Software Analysis, Evolution, and Reengineering (SANER)","volume":"1","author":"Beller Moritz","year":"2016","unstructured":"Moritz Beller, Radjino Bholanath, Shane McIntosh, and Andy Zaidman. 2016. Analyzing the state of static analysis: A large-scale evaluation in open source software. In Proceedings of the 2016 IEEE 23rd International Conference on Software Analysis, Evolution, and Reengineering (SANER), Vol. 1, 470\u2013481. DOI: 10.1109\/SANER.2016.105"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99527-0_20"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30820-8_29"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57256-2_15"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.233.6"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-017-0469-y"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.14236\/ewic\/VOCS2008.32"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375591"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/2984450.2984457"},{"key":"e_1_3_3_17_2","first-page":"209","volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI \u201908)","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI \u201908). USENIX Association, USA, 209\u2013224. Retrieved from https:\/\/www.usenix.org\/legacy\/events\/osdi08\/tech\/full_papers\/cadar\/cadar.pdf"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523720"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3507473.3507475"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/2970276.2970347"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926399"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_34"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74061-2_27"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICPP.2015.98"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30820-8_40"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/945445.945468"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/502034.502041"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523727"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17502-3_15"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3240481"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3196398.3196451"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_19"},{"key":"e_1_3_3_33_2","first-page":"1","volume-title":"Proceedings of the ACM on Programming Languages 3, POPL","volume":"57","author":"Gorogiannis Nikos","year":"2019","unstructured":"Nikos Gorogiannis, Peter W. O\u2019Hearn, and Ilya Sergey. 2019. A true positives theorem for a static race detector. Proceedings of the ACM on Programming Languages 3, POPL (Jan. 2019), 57:1\u201357:29. DOI: 10.1145\/3290370"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66706-5_7"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_19"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454108"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99527-0_25"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30820-8_39"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/379605.379665"},{"key":"e_1_3_3_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3689492.3690053"},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.15256095Artifact"},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00069"},{"issue":"1999","key":"e_1_3_3_44_2","article-title":"ISO\/IEC","volume":"9899","author":"ISO\/IEC.","unstructured":"ISO\/IEC. 1999. Programming languages\u2014C. ISO\/IEC 9899:1999. Retrieved from https:\/\/www.iso.org\/standard\/29237.htmlInternational Standard","journal-title":"Programming languages\u2014C"},{"key":"e_1_3_3_45_2","unstructured":"ISO\/IEC. 2011. ISO International Standard ISO\/IEC 9899:2011."},{"key":"e_1_3_3_46_2","doi-asserted-by":"crossref","first-page":"672","DOI":"10.1109\/ICSE.2013.6606613","volume-title":"Proceedings of the 2013 International Conference on Software Engineering (ICSE \u201913)","author":"Johnson Brittany","year":"2013","unstructured":"Brittany Johnson, Yoonki Song, Emerson Murphy-Hill, and Robert Bowdidge. 2013. Why don\u2019t software developers use static analysis tools to find bugs?. In Proceedings of the 2013 International Conference on Software Engineering (ICSE \u201913). IEEE Press, Piscataway, NJ, 672\u2013681. Retrieved from https:\/\/dl.acm.org\/doi\/10.5555\/2486788.2486877"},{"key":"e_1_3_3_47_2","volume-title":"The Rust Programming Language","author":"Klabnik Steve","year":"2024","unstructured":"Steve Klabnik and Carol Nichols. 2024. The Rust Programming Language. No Starch Press."},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99527-0_35"},{"key":"e_1_3_3_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/3527325"},{"key":"e_1_3_3_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/3126908.3126958"},{"key":"e_1_3_3_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009857"},{"key":"e_1_3_3_52_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2015.87"},{"key":"e_1_3_3_53_2","first-page":"63","volume-title":"Workshop on the Evaluation of Software Defect Detection Tools","author":"Lu Shan","year":"2005","unstructured":"Shan Lu, Zhenmin Li, Feng Qin, Lin Tan, Pin Zhou, and Yuanyuan Zhou. 2005. BugBench: benchmarks for evaluating bug detection tools. In Workshop on the Evaluation of Software Defect Detection Tools, Vol. 5. Chicago, Illinois. Retrieved from https:\/\/www.cs.umd.edu\/\u223cpugh\/BugWorkshop05\/papers\/63-lu.pdf"},{"key":"e_1_3_3_54_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(1:26)2012"},{"key":"e_1_3_3_55_2","doi-asserted-by":"crossref","unstructured":"Rapha\u00ebl Monat Abdelraouf Ouadjaout and Antoine Min\u00e9. 2024. Easing maintenance of academic static analyzers. International\u00a0Journal on Software Tools for Technology Transfer\u00a026 (2024) 673\u2013686.\u00a0DOI: https:\/\/doi.org\/10.1007\/s10009-024-00770-1","DOI":"10.1007\/s10009-024-00770-1"},{"key":"e_1_3_3_56_2","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190265"},{"key":"e_1_3_3_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03427-6_14"},{"key":"e_1_3_3_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_3_3_59_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45237-7_24"},{"key":"e_1_3_3_60_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72013-1_26"},{"key":"e_1_3_3_61_2","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134019"},{"key":"e_1_3_3_62_2","doi-asserted-by":"publisher","DOI":"10.1145\/1889997.1890000"},{"key":"e_1_3_3_63_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386036"},{"key":"e_1_3_3_64_2","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186041"},{"key":"e_1_3_3_65_2","doi-asserted-by":"publisher","DOI":"10.1145\/349214.349241"},{"key":"e_1_3_3_66_2","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254104"},{"key":"e_1_3_3_67_2","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_21"},{"key":"e_1_3_3_68_2","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884835"},{"key":"e_1_3_3_69_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30820-8_34"},{"key":"e_1_3_3_70_2","unstructured":"SAMATE. 2021. Static analysis tool exposition (SATE).Retrieved 16 November 2023 from https:\/\/www.nist.gov\/itl\/ssd\/software-quality-group\/samate\/static-analysis-tool-exposition-sate"},{"key":"e_1_3_3_71_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_3_3_72_2","first-page":"1361","volume-title":"Proceedings of the 2013 Federated Conference on Computer Science and Information Systems (FedCSIS \u201913)","author":"Schimmel Jochen","year":"2013","unstructured":"Jochen Schimmel, Korbinian Molitorisz, and Walter F. Tichy. 2013. An evaluation of data race detectors using bug repositories. In Proceedings of the 2013 Federated Conference on Computer Science and Information Systems (FedCSIS \u201913), 1361\u20131364. Retrieved from https:\/\/ieeexplore.ieee.org\/document\/6644193"},{"key":"e_1_3_3_73_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-024-00773-y"},{"key":"e_1_3_3_74_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-88806-0_18"},{"key":"e_1_3_3_75_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-56222-8_16"},{"key":"e_1_3_3_76_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03237-0_13"},{"key":"e_1_3_3_77_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_41"},{"key":"e_1_3_3_78_2","doi-asserted-by":"publisher","DOI":"10.1145\/1791194.1791203"},{"key":"e_1_3_3_79_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29860-8_9"},{"key":"e_1_3_3_80_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2015.24"},{"key":"e_1_3_3_81_2","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180236"},{"key":"e_1_3_3_82_2","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375583"},{"key":"e_1_3_3_83_2","unstructured":"The Open Group. 1997. pthread_cond_wait. Retrieved from https:\/\/pubs.opengroup.org\/onlinepubs\/7908799\/xsh\/pthread_cond_wait.html"},{"key":"e_1_3_3_84_2","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102257"},{"key":"e_1_3_3_85_2","doi-asserted-by":"publisher","DOI":"10.1145\/3297858.3304069"},{"key":"e_1_3_3_86_2","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2307.14909"},{"key":"e_1_3_3_87_2","volume-title":"Static Data Race Analysis of Heap-Manipulating C Programs","author":"Vojdani Vesal","year":"2010","unstructured":"Vesal Vojdani. 2010. Static Data Race Analysis of Heap-Manipulating C Programs. Ph.\u2009D. Dissertation. University of Tartu. Retrieved from http:\/\/hdl.handle.net\/10062\/15866"},{"key":"e_1_3_3_88_2","doi-asserted-by":"publisher","DOI":"10.1145\/2970276.2970337"},{"issue":"2009","key":"e_1_3_3_89_2","first-page":"141","article-title":"Goblint: Path-sensitive data race analysis","volume":"30","author":"Vojdani Vesal","year":"2009","unstructured":"Vesal Vojdani and Varmo Vene. 2009. Goblint: Path-sensitive data race analysis. Annales Universitatis Scientiarum Budapestinensis de Rolando E\u00f6tv\u00f6s Nominatae. Sectio Computatorica 30 (2009), 141\u2013155. http:\/\/ac.inf.elte.hu\/Vol_030_2009\/141.pdf","journal-title":"Annales Universitatis Scientiarum Budapestinensis de Rolando E\u00f6tv\u00f6s Nominatae. Sectio Computatorica"},{"key":"e_1_3_3_90_2","doi-asserted-by":"publisher","DOI":"10.1145\/1287624.1287654"},{"key":"e_1_3_3_91_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2014.44"},{"key":"e_1_3_3_92_2","doi-asserted-by":"publisher","DOI":"10.1504\/IJHPCN.2017.086532"},{"key":"e_1_3_3_93_2","doi-asserted-by":"publisher","DOI":"10.1145\/3611643.3616272"},{"key":"e_1_3_3_94_2","doi-asserted-by":"publisher","DOI":"10.1145\/3168813"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3732933","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T13:53:59Z","timestamp":1757944439000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3732933"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,15]]},"references-count":93,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9,30]]}},"alternative-id":["10.1145\/3732933"],"URL":"https:\/\/doi.org\/10.1145\/3732933","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,15]]},"assertion":[{"value":"2024-08-21","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-08","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-09-15","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}