Online efficient predictive safety analysis of multithreaded programs
By
We present an automated and configurable technique for runtime safety analysis of multithreaded programs that is able to predict safety violations from successful executions. Based on a formal specification of safety properties provided by a user, our technique enables us to automatically instrument a given program and create an observer so that the program emits relevant state update events to the observer and the observer checks these updates against the safety specification. The events are stamped with dynamic vector clocks, enabling the observer to infer a causal partial order on the state updates. All event traces that are consistent with this partial order, including the actual execution trace, are then analyzed online and in parallel. A warning is issued whenever one of these potential traces violates the specification. Our technique is scalable and can provide better coverage than conventional testing, but its coverage need not be exhaustive. In fact, one can trade off scalability and comprehensiveness: a window in the state space may be specified allowing the observer to infer some of the more likely runs; if the size of the window is 1, then only the actual execution trace is analyzed, as is the case in conventional testing; if the size of the window is ∞, then all the execution traces consistent with the actual execution trace are analyzed.
Keywords Predictive analysis - Vector clock - Runtime monitoring - JMPaX - Multithreaded analysis
BibTeX
@article{journals/sttt/SenRA06,
author = "Sen, Koushik and Rosu, Grigore and Agha, Gul",
title = "Online efficient predictive safety analysis of
multithreaded programs",
ee = "http://dx.doi.org/10.1007/s10009-005-0192-y",
journal = "STTT",
keywords = "formal methods, software engineering",
number = "3",
pages = "248-260",
volume = "8",
year = "2006",
}