Sciweavers

Share
TACAS
2010
Springer

Trace-Based Symbolic Analysis for Atomicity Violations

10 years 17 days ago
Trace-Based Symbolic Analysis for Atomicity Violations
Abstract. We propose a symbolic algorithm to accurately predict atomicity violations by analyzing a concrete execution trace of a concurrent program. We use both the execution trace and the program source code to construct a symbolic predictive model, which captures a large set of alternative interleavings of the events of the given trace. We use precise symbolic reasoning with a satisfiability modulo theory (SMT) solver to check the feasible interleavings for atomicity violations. Our algorithm differs from the existing methods in that all reported atomicity violations can appear in the actual program execution; and at the same time the feasible interleavings analyzed by our model are significantly more than other predictive models that guarantee the absence of false alarms.
Chao Wang, Rhishikesh Limaye, Malay K. Ganai, Aart
Added 14 May 2010
Updated 14 May 2010
Type Conference
Year 2010
Where TACAS
Authors Chao Wang, Rhishikesh Limaye, Malay K. Ganai, Aarti Gupta
Comments (0)
books