Online Efficient Predictive Safety Analysis of Multithreaded Programs
Abstract
An automated and configurable technique for runtime safety analysis of multithreaded programs is presented, which is able to predict safety violations from successful executions. Based on a user provided safety formal specification, the program is automatically instrumented to emit relevant state update events to an observer, which further checks them 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 analyzed on-line and in parallel, and a warning is issued whenever there is a trace violating the specification. This technique can be therefore seen as a bridge between testing and model checking. To further increase scalability, a window in the state space can be specified, allowing the observer to infer the most probable runs. If the size of the window is 1 then only the received execution trace is analyzed, like in testing; if the size of the window is then all the execution traces are analyzed, such as in model checking.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 2005
- Accession Number
- ADA483547
Entities
People
- Grigore Rosu
- Gul Agha
- Koushik Sen
Organizations
- University of Illinois Urbana–Champaign