Maximal sound predictive race detection with control flow abstraction

Jeff Huang, Patrick O.Neil Meredith, Grigore Rosu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Despite the numerous static and dynamic program analysis techniques in the literature, data races remain one of the most common bugs in modern concurrent software. Further, the techniques that do exist either have limited detection capability or are unsound, meaning that they report false positives. We present a sound race detection technique that achieves a provably higher detection capability than existing sound techniques. A key insight of our technique is the inclusion of abstracted control flow information into the execution model, which increases the space of the causal model permitted by classical happens-before or causally-precedes based detectors. By encoding the control flow and a minimal set of feasibility constraints as a group of first-order logic formulae, we formulate race detection as a constraint solving problem. Moreover, we formally prove that our formulation achieves the maximal possible detection capability for any sound dynamic race detector with respect to the same input trace under the sequential consistency memory model. We demonstrate via extensive experimentation that our technique detects more races than the other state-of-the-art sound race detection techniques, and that it is scalable to executions of real world concurrent applications with tens of millions of critical events. These experiments also revealed several previously unknown races in real systems (e.g., Eclipse) that have been confirmed or fixed by the developers. Our tool is also adopted by Eclipse developers.

Original languageEnglish (US)
Title of host publicationPLDI 2014 - Proceedings of the 2014 ACM SIGPLAN Conference on Programming Language Design and Implementation
PublisherAssociation for Computing Machinery
Pages337-348
Number of pages12
ISBN (Print)9781450327848
DOIs
StatePublished - 2014
Event35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014 - Edinburgh, United Kingdom
Duration: Jun 9 2014Jun 11 2014

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

Other

Other35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014
CountryUnited Kingdom
CityEdinburgh
Period6/9/146/11/14

Keywords

  • Control flow
  • Data race
  • Maximal sound
  • Prediction

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Maximal sound predictive race detection with control flow abstraction'. Together they form a unique fingerprint.

Cite this