Sound predictive race detection in polynomial time

Data races are among the most reliable indicators of programming errors in concurrent software. For at least two decades, Lamport’s happens-before (HB) relation has served as the standard test for detecting races—other techniques, such as lockset-based approaches, fail to be sound, as they may falsely warn of races. This work introduces a new relation, causally-precedes (CP), which generalizes happens-before to observe more races without sacrificing soundness. Intuitively, CP tries to capture the concept of happens-before ordered events that must occur in the observed order for the program to observe the same values. What distinguishes CP from past predictive race detection approaches (which also generalize an observed execution to detect races in other plausible executions) is that CP-based race detection is both sound and of polynomial complexity. We demonstrate that the unique aspects of CP result in practical benefit. Applying CP to real-world programs, we successfully analy...

• Type: Journal
• Year: 2012
• Where: POPL
• Authors: Yannis Smaragdakis, Jacob Evans, Caitlin Sadowski, Jaeheon Yi, Cormac Flanagan
• Keywords: Concurrent Software, Ftpserver, Polynomial Complexity, POPL 2012, Programming Languages