Online efficient predictive safety analysis of multithreaded programs

Koushik Sen, Grigore Roşu, Gul Agha

Research output: Contribution to journalArticlepeer-review

Abstract

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.

Original languageEnglish (US)
Pages (from-to)248-260
Number of pages13
JournalInternational Journal on Software Tools for Technology Transfer
Volume8
Issue number3
DOIs
StatePublished - Jun 1 2006

Keywords

  • JMPaX
  • Multithreaded analysis
  • Predictive analysis
  • Runtime monitoring
  • Vector clock

ASJC Scopus subject areas

  • Software
  • Information Systems

Fingerprint

Dive into the research topics of 'Online efficient predictive safety analysis of multithreaded programs'. Together they form a unique fingerprint.

Cite this