Detecting errors in multithreaded programs by generalized predictive analysis of executions

By

Full Text:
http://dx.doi.org/10.1007/11494881_14

Abstract

A predictive runtime analysis technique is proposed for detecting violations of safety properties from apparently successful executions of concurrent systems. In this paper we focus on concurrent systems developed using common object-oriented multithreaded programming languages, in particular, Java. Specifically, we provide an algorithm to observe execution traces of multithreaded programs and, based on appropriate code instrumentation that allows one to atomically extract a partial-order causality from a linear sequence of events, we predict other schedules that are compatible with the run. The technique uses a weak happens-before relation which orders a write of a shared variable with all its subsequent reads that occur before the next write to the variable. A permutation of the observed events is a possible execution of a program if and only if it does not contradict the weak happens-before relation. Even though an observed execution trace may not violate the given specification, our algorithm infers other possible executions (consistent with the observed execution) that violate the given specification, if such an execution exists. Therefore, it can predict concurrency errors from non-violating runs.

BibTeX

@inproceedings{conf/fmoods/SenRA05,
author = "Sen, Koushik and Rosu, Grigore and Agha, Gul",
editor = "Steffen, Martin and Zavattaro, Gianluigi",
title = "Detecting Errors in Multithreaded Programs by Generalized
Predictive Analysis of Executions",
booktitle = "FMOODS",
crossref = "conf/fmoods/2005",
ee = "http://dx.doi.org/10.1007/11494881_14",
keywords = "formal methods, software engineering",
pages = "211-226",
year = "2005",
}

@proceedings{conf/fmoods/2005,
editor = "Steffen, Martin and Zavattaro, Gianluigi",
title = "Formal Methods for Open Object-Based Distributed Systems,
7th IFIP WG 6.1 International Conference, FMOODS 2005, Athens,
Greece, June 15-17, 2005, Proceedings",
isbn = "3-540-26181-8",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
volume = "3535",
year = "2005",
}