Error invariants for concurrent traces

Andreas Holzer, Daniel Schwartz-Narbonne, Mitra Tabaei Befrouei, Georg Weissenbacher, Thomas Wies

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Error invariants are assertions that over-approximate the reachable program states at a given position in an error trace while only capturing states that will still lead to failure if execution of the trace is continued from that position. Such assertions reflect the effect of statements that are involved in the root cause of an error and its propagation, enabling slicing of statements that do not contribute to the error. Previous work on error invariants focused on sequential programs. We generalize error invariants to concurrent traces by augmenting them with additional information about hazards such as write-after-write events, which are often involved in race conditions and atomicity violations. By providing the option to include varying levels of details in error invariants—such as hazards and branching information—our approach allows the programmer to systematically analyze individual aspects of an error trace. We have implemented a hazard-sensitive slicing tool for concurrent traces based on error invariants and evaluated it on benchmarks covering a broad range of real-world concurrency bugs. Hazard-sensitive slicing significantly reduced the length of the considered traces and still maintained the root causes of the concurrency bugs.

Original languageEnglish (US)
Title of host publicationFM 2016: Formal Methods - 21st International Symposium, Proceedings
PublisherSpringer Verlag
Pages370-387
Number of pages18
Volume9995 LNCS
ISBN (Print)9783319489889
DOIs
StatePublished - 2016
Event21st International Symposium on Formal Methods, FM 2016 - Limassol, Cyprus
Duration: Nov 9 2016Nov 11 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9995 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other21st International Symposium on Formal Methods, FM 2016
CountryCyprus
CityLimassol
Period11/9/1611/11/16

Fingerprint

Concurrent
Trace
Invariant
Hazard
Slicing
Hazards
Concurrency
Assertion
Hazards and race conditions
Roots
Atomicity
Branching
Covering
Propagation
Benchmark
Generalise
Range of data

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Holzer, A., Schwartz-Narbonne, D., Befrouei, M. T., Weissenbacher, G., & Wies, T. (2016). Error invariants for concurrent traces. In FM 2016: Formal Methods - 21st International Symposium, Proceedings (Vol. 9995 LNCS, pp. 370-387). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9995 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-48989-6_23

Error invariants for concurrent traces. / Holzer, Andreas; Schwartz-Narbonne, Daniel; Befrouei, Mitra Tabaei; Weissenbacher, Georg; Wies, Thomas.

FM 2016: Formal Methods - 21st International Symposium, Proceedings. Vol. 9995 LNCS Springer Verlag, 2016. p. 370-387 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9995 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Holzer, A, Schwartz-Narbonne, D, Befrouei, MT, Weissenbacher, G & Wies, T 2016, Error invariants for concurrent traces. in FM 2016: Formal Methods - 21st International Symposium, Proceedings. vol. 9995 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9995 LNCS, Springer Verlag, pp. 370-387, 21st International Symposium on Formal Methods, FM 2016, Limassol, Cyprus, 11/9/16. https://doi.org/10.1007/978-3-319-48989-6_23
Holzer A, Schwartz-Narbonne D, Befrouei MT, Weissenbacher G, Wies T. Error invariants for concurrent traces. In FM 2016: Formal Methods - 21st International Symposium, Proceedings. Vol. 9995 LNCS. Springer Verlag. 2016. p. 370-387. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-48989-6_23
Holzer, Andreas ; Schwartz-Narbonne, Daniel ; Befrouei, Mitra Tabaei ; Weissenbacher, Georg ; Wies, Thomas. / Error invariants for concurrent traces. FM 2016: Formal Methods - 21st International Symposium, Proceedings. Vol. 9995 LNCS Springer Verlag, 2016. pp. 370-387 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{7e1af2c3def346d188f1a4bfe40fd4cd,
title = "Error invariants for concurrent traces",
abstract = "Error invariants are assertions that over-approximate the reachable program states at a given position in an error trace while only capturing states that will still lead to failure if execution of the trace is continued from that position. Such assertions reflect the effect of statements that are involved in the root cause of an error and its propagation, enabling slicing of statements that do not contribute to the error. Previous work on error invariants focused on sequential programs. We generalize error invariants to concurrent traces by augmenting them with additional information about hazards such as write-after-write events, which are often involved in race conditions and atomicity violations. By providing the option to include varying levels of details in error invariants—such as hazards and branching information—our approach allows the programmer to systematically analyze individual aspects of an error trace. We have implemented a hazard-sensitive slicing tool for concurrent traces based on error invariants and evaluated it on benchmarks covering a broad range of real-world concurrency bugs. Hazard-sensitive slicing significantly reduced the length of the considered traces and still maintained the root causes of the concurrency bugs.",
author = "Andreas Holzer and Daniel Schwartz-Narbonne and Befrouei, {Mitra Tabaei} and Georg Weissenbacher and Thomas Wies",
year = "2016",
doi = "10.1007/978-3-319-48989-6_23",
language = "English (US)",
isbn = "9783319489889",
volume = "9995 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "370--387",
booktitle = "FM 2016: Formal Methods - 21st International Symposium, Proceedings",
address = "Germany",

}

TY - GEN

T1 - Error invariants for concurrent traces

AU - Holzer, Andreas

AU - Schwartz-Narbonne, Daniel

AU - Befrouei, Mitra Tabaei

AU - Weissenbacher, Georg

AU - Wies, Thomas

PY - 2016

Y1 - 2016

N2 - Error invariants are assertions that over-approximate the reachable program states at a given position in an error trace while only capturing states that will still lead to failure if execution of the trace is continued from that position. Such assertions reflect the effect of statements that are involved in the root cause of an error and its propagation, enabling slicing of statements that do not contribute to the error. Previous work on error invariants focused on sequential programs. We generalize error invariants to concurrent traces by augmenting them with additional information about hazards such as write-after-write events, which are often involved in race conditions and atomicity violations. By providing the option to include varying levels of details in error invariants—such as hazards and branching information—our approach allows the programmer to systematically analyze individual aspects of an error trace. We have implemented a hazard-sensitive slicing tool for concurrent traces based on error invariants and evaluated it on benchmarks covering a broad range of real-world concurrency bugs. Hazard-sensitive slicing significantly reduced the length of the considered traces and still maintained the root causes of the concurrency bugs.

AB - Error invariants are assertions that over-approximate the reachable program states at a given position in an error trace while only capturing states that will still lead to failure if execution of the trace is continued from that position. Such assertions reflect the effect of statements that are involved in the root cause of an error and its propagation, enabling slicing of statements that do not contribute to the error. Previous work on error invariants focused on sequential programs. We generalize error invariants to concurrent traces by augmenting them with additional information about hazards such as write-after-write events, which are often involved in race conditions and atomicity violations. By providing the option to include varying levels of details in error invariants—such as hazards and branching information—our approach allows the programmer to systematically analyze individual aspects of an error trace. We have implemented a hazard-sensitive slicing tool for concurrent traces based on error invariants and evaluated it on benchmarks covering a broad range of real-world concurrency bugs. Hazard-sensitive slicing significantly reduced the length of the considered traces and still maintained the root causes of the concurrency bugs.

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

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

U2 - 10.1007/978-3-319-48989-6_23

DO - 10.1007/978-3-319-48989-6_23

M3 - Conference contribution

SN - 9783319489889

VL - 9995 LNCS

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

SP - 370

EP - 387

BT - FM 2016: Formal Methods - 21st International Symposium, Proceedings

PB - Springer Verlag

ER -