Runtime safety analysis of multithreaded programs

By Koushik Sen, Grigore Rosu, and Gul Agha. In ESEC / SIGSOFT FSE, 337–346. ACM, 2003.

Full Text:: Download PDF
Publisher Link:: http://doi.acm.org/10.1145/940071.940116

Abstract

Foundational and scalable techniques for runtime safety analysis of multithreaded programs are explored in this paper. A technique based on vector clocks to extract the causal dependency order on state updates from a running multithreaded program is presented, together with algorithms to analyze a multithreaded computation against safety properties expressed using temporal logics. A prototype tool implementing our techniques, is also presented, together with examples where it can predict safety errors in multithreaded programs from successful executions of those programs. This tool is called Java MultiPathExplorer (JMPaX), and available for download on the web. To the best of our knowledge, JMPaX is the first tool of its kind.

BibTeX

@inproceedings{conf/sigsoft/SenRA03,
    author = "Sen, Koushik and Rosu, Grigore and Agha, Gul",
    title = "Runtime safety analysis of multithreaded programs",
    booktitle = "ESEC / SIGSOFT FSE",
    crossref = "conf/sigsoft/2003",
    ee = "http://doi.acm.org/10.1145/940071.940116",
    keywords = "formal methods, sensor networks, real-time systems,
                software engineering",
    pages = "337-346",
    year = "2003",
}

@proceedings{conf/sigsoft/2003,
    title = "Proceedings of the 11th ACM SIGSOFT Symposium on
             Foundations of Software Engineering 2003 held jointly with 9th
             European Software Engineering Conference, ESEC/FSE 2003, Helsinki,
             Finland, September 1-5, 2003",
    publisher = "ACM",
    year = "2003",
}