Περίληψη:
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 analyze
server-level applications (e. g., Apache FtpServer) and show that traces
longer than in past predictive race analyses can be analyzed in mere
seconds to a few minutes. For these programs, CP race detection uncovers
races that are hard to detect by repeated execution and HB race
detection: a single run of CP race detection produces several races not
discovered by 10 separate rounds of happens-before race detection.
Συγγραφείς:
Smaragdakis, Yannis
Evans, Jacob M.
Sadowski, Caitlin
Yi,
Jaeheon
Flanagan, Cormac
