Sciweavers

Share
FM
2009
Springer

Symbolic Predictive Analysis for Concurrent Programs

10 years 7 days ago
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...
Chao Wang, Sudipta Kundu, Malay K. Ganai, Aarti Gu
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where FM
Authors Chao Wang, Sudipta Kundu, Malay K. Ganai, Aarti Gupta
Comments (0)
books