Open Systems Laboratory at Illinois

Online efficient predictive safety analysis of multithreaded programs

By Koushik Sen, Grigore Rosu, and Gul Agha. In TACAS, volume 2988 of Lecture Notes in Computer Science, 123–138. Springer, 2004.

Full Text:
Download PDF
Publisher Link:


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.


    author = "Sen, Koushik and Rosu, Grigore and Agha, Gul",
    editor = "Jensen, Kurt and Podelski, Andreas",
    title = "Online Efficient Predictive Safety Analysis of
             Multithreaded Programs",
    booktitle = "TACAS",
    crossref = "conf/tacas/2004",
    ee = "",
    keywords = "formal methods, sensor networks, real-time systems",
    pages = "123-138",
    year = "2004",

    editor = "Jensen, Kurt and Podelski, Andreas",
    title = "Tools and Algorithms for the Construction and Analysis of
             Systems, 10th International Conference, TACAS 2004, Held as Part
             of the Joint European Conferences on Theory and Practice of
             Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004,
    isbn = "3-540-21299-X",
    publisher = "Springer",
    series = "Lecture Notes in Computer Science",
    volume = "2988",
    year = "2004",