Detecting errors in multithreaded programs by generalized predictive analysis of executions

Koushik Sen, Grigore Roşu, Gul Agha

Research output: Contribution to journalConference article

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.

Original languageEnglish (US)
Pages (from-to)211-226
Number of pages16
JournalLecture Notes in Computer Science
Volume3535
StatePublished - Oct 17 2005
Event7th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2005 - Athens, Greece
Duration: Jun 15 2005Jun 17 2005

Fingerprint

Concurrent Systems
Violate
Trace
Runtime Analysis
Specification
Specifications
Predict
Object-oriented Languages
Order Relation
Object-oriented Programming
Object oriented programming
Causality
Concurrency
Partial Order
Instrumentation
Computer programming languages
Java
Programming Languages
Permutation
Schedule

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Detecting errors in multithreaded programs by generalized predictive analysis of executions. / Sen, Koushik; Roşu, Grigore; Agha, Gul.

In: Lecture Notes in Computer Science, Vol. 3535, 17.10.2005, p. 211-226.

Research output: Contribution to journalConference article

@article{3e2d8e40147140df85e635807e16430e,
title = "Detecting errors in multithreaded programs by generalized predictive analysis of executions",
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.",
author = "Koushik Sen and Grigore Roşu and Gul Agha",
year = "2005",
month = "10",
day = "17",
language = "English (US)",
volume = "3535",
pages = "211--226",
journal = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
issn = "0302-9743",
publisher = "Springer Verlag",

}

TY - JOUR

T1 - Detecting errors in multithreaded programs by generalized predictive analysis of executions

AU - Sen, Koushik

AU - Roşu, Grigore

AU - Agha, Gul

PY - 2005/10/17

Y1 - 2005/10/17

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=26444458411&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=26444458411&partnerID=8YFLogxK

M3 - Conference article

AN - SCOPUS:26444458411

VL - 3535

SP - 211

EP - 226

JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SN - 0302-9743

ER -