[TOPLAS] Sound Static Data Race Verification for C: Is the Race Lost?
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 JunDisplayed time zone: Seoul change
14:00 - 15:20 | |||
14:00 20mTalk | 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 20mTalk | 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 20mTalk | [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 20mTalk | Nola: Later-Free Ghost State for Verifying Termination in Iris PLDI Research Papers Link to publication DOI |