PLDI 2025
Mon 16 - Fri 20 June 2025 Seoul, South Korea
Fri 20 Jun 2025 14:40 - 15:00 at Cosmos, Violet & Tulip - Concurrency Chair(s): Jeehoon Kang

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, SVCOMP. 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 7 tools failed to return any result on any real-world benchmarks under our chosen resource limitations, with the remaining 2 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.

Fri 20 Jun

Displayed time zone: Seoul change

14:00 - 15:20
14:00
20m
Talk
Efficient Timestamping for Sampling-Based Race Detection
PLDI Research Papers
Minjian Zhang University of Illinois at Urbana-Champaign, Daniel Wee Soong Lim National University of Singapore, Mosaad Al Thokair Saudi Aramco, Umang Mathur National University of Singapore, Mahesh Viswanathan University of Illinois at Urbana-Champaign
DOI Pre-print
14:20
20m
Talk
Efficient Linearizability Monitoring
PLDI Research Papers
Parosh Aziz Abdulla Uppsala University; Mälardalen University, Samuel Grahn Uppsala University, Bengt Jonsson Uppsala University, Shankaranarayanan Krishna IIT Bombay, Om Swostik Mishra IIT Bombay
DOI
14:40
20m
Talk
[TOPLAS] Sound Static Data Race Verification for C: Is the Race Lost?
PLDI Research Papers
Karoliine Holter University of Tartu, Estonia, Simmo Saan University of Tartu, Estonia, Patrick Lam University of Waterloo, Vesal Vojdani University of Tartu
DOI Pre-print
15:00
20m
Talk
Nola: Later-Free Ghost State for Verifying Termination in Iris
PLDI Research Papers
Yusuke Matsushita Kyoto University, Takeshi Tsukada Chiba University
Link to publication DOI