Symbolic Predictive Analysis for Concurrent Programs

Abstract. Predictive analysis aims at detecting concurrency errors during runtime by monitoring a concrete execution trace of a concurrent program. In recent years, various models based on happens-before causality relations have been proposed for predictive analysis to improve the interleaving coverage while ensuring the absence of false alarms. However, these models are based on only the observed events, and typically do not utilize source code. Furthermore, the enumerative algorithms they use for verifying safety properties in the predicted execution traces often suffer from the interleaving explosion problem. In this paper, we introduce a new symbolic causal model based on source code and the observed events, and propose a symbolic algorithm to check whether a safety property holds in all feasible permutations of events in the given execution trace. Rather than explicitly enumerating the interleavings, our algorithm conducts the verification using a novel encoding of the causal mod...

• Type: Conference
• Year: 2009
• Where: FM
• Authors: Chao Wang, Sudipta Kundu, Malay K. Ganai, Aarti Gupta
• Keywords: Causal Models, Execution Trace, FM 2009, Interleaving Coverage, Natural Language Processing