Maximal Causal Models for Multithreaded Systems

PLDI'14

Maximal Sound Predictive Race Detection with Control Flow Abstraction

Jeff Huang and Patrick Meredith and Grigore Rosu

PLDI'14, ACM, pp 337-348. 2014

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.

PDF, Slides(PPT), Slides(PDF), jPredictor, DOI, PLDI'14, BIB

RV'12

Maximal Causal Models for Sequentially Consistent Systems

Traian Florin Serbanuta and Feng Chen and Grigore Rosu

RV'12, LNCS 7687, pp 136-150. 2012

Abstract. This paper shows that it is possible to build a maximal and sound causal model for concurrent computations from a given execution trace. It is sound, in the sense that any program which can generate a trace can also generate all traces in its causal model. It is maximal (among sound models), in the sense that by extending the causal model of an observed trace with a new trace, the model becomes unsound: there exists a program generating the original trace which cannot generate the newly introduced trace. Thus, the maximal sound model has the property that it comprises all traces which all programs that can generate the original trace can also generate. The existence of such a model is of great theoretical value as it can be used to prove the soundness of non-maximal, and thus smaller, causal models.

PDF, Slides(PDF), JPredictor, DOI, RV'12, BIB

Technical Report 2011

Maximal Causal Models for Sequentially Consistent Systems

Traian Florin Serbanuta and Feng Chen and Grigore Rosu

Technical Report http://hdl.handle.net/2142/27708, October 2011

Abstract. This paper shows that it is possible to build a maximal and sound causal model for concurrent computations from a given execution trace. It is sound, in the sense that any program which can generate a trace can also generate all traces in its causal model. It is maximal (among sound models), in the sense that by extending the causal model of an observed trace with a new trace, the model becomes unsound: there exists a program generating the original trace which cannot generate the newly introduced trace. Thus, the maximal sound model has the property that it comprises all traces which all programs that can generate the original trace can also generate. The existence of such a model is of great theoretical value. First, it can be used to prove the soundness of non-maximal, and thus smaller, causal models. Second, since it is maximal, the proposed model allows for natural and causal-model-independent definitions of trace-based properties; this paper proposes maximal definitions for causal dataraces and causal atomicity. Finally, although defined axiomatically, the set of traces comprised by the proposed model are shown to be effectively constructed from the original trace. Thus, maximal causal models are also amenable for developing practical analysis tools.

PDF, JPredictor, DOI, BIB