Run-time Assertion Checking of JML Annotations in Multithreaded Applications with e-OpenJML

Jorne Kandziora, Marieke Huisman, Christoph Bockisch, M. Zaharieva

  • 1 Citations

Abstract

Run-time assertion checking of multithreaded programs is challenging, as assertion evaluation should not interfere with the execution of other threads. This paper describes the prototype implementation of a run-time assertion checker that achieves this by evaluating assertions over snapshots of the state, instead of over the live state. Our prototype e-OpenJML, an extension to OpenJML, provides an easy to use, safe and interference-free evaluation of JML specifications in multithreaded programs. To achieve this, it integrates e-STROBE, our extension to the STROBE framework for asynchronous assertion evaluation. e-STROBE prevents all possible interferences between assertion evaluation and other program threads, which the original STROBE can not. It also simplifies evaluating assertions that relate the value of expressions in multiple states.
Original languageUndefined
Title of host publicationProceedings of the 17th Workshop on Formal Techniques for Java-like Programs (FTfJP 2015)
EditorsR. Monahan
Place of PublicationNew York
PublisherAssociation for Computing Machinery (ACM)
Pages8
Number of pages6
ISBN (Print)978-1-4503-3656-7
DOIs
StatePublished - Jul 2015
Event17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015 - Prague, Czech Republic

Publication series

Name
PublisherACM

Workshop

Workshop17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015
Abbreviated titleFTfJP
CountryCzech Republic
CityPrague
Period7/07/157/07/15
Internet address

Fingerprint

Specifications

Keywords

  • EWI-26138
  • METIS-312668
  • IR-96983

Cite this

Kandziora, J., Huisman, M., Bockisch, C., & Zaharieva, M. (2015). Run-time Assertion Checking of JML Annotations in Multithreaded Applications with e-OpenJML. In R. Monahan (Ed.), Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs (FTfJP 2015) (pp. 8). [8] New York: Association for Computing Machinery (ACM). DOI: 10.1145/2786536.2786541

Kandziora, Jorne; Huisman, Marieke; Bockisch, Christoph; Zaharieva, M. / Run-time Assertion Checking of JML Annotations in Multithreaded Applications with e-OpenJML.

Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs (FTfJP 2015). ed. / R. Monahan. New York : Association for Computing Machinery (ACM), 2015. p. 8 8.

Research output: Scientific - peer-reviewConference contribution

@inbook{daa68a9d5f1540f6897963e5ea0c514e,
title = "Run-time Assertion Checking of JML Annotations in Multithreaded Applications with e-OpenJML",
abstract = "Run-time assertion checking of multithreaded programs is challenging, as assertion evaluation should not interfere with the execution of other threads. This paper describes the prototype implementation of a run-time assertion checker that achieves this by evaluating assertions over snapshots of the state, instead of over the live state. Our prototype e-OpenJML, an extension to OpenJML, provides an easy to use, safe and interference-free evaluation of JML specifications in multithreaded programs. To achieve this, it integrates e-STROBE, our extension to the STROBE framework for asynchronous assertion evaluation. e-STROBE prevents all possible interferences between assertion evaluation and other program threads, which the original STROBE can not. It also simplifies evaluating assertions that relate the value of expressions in multiple states.",
keywords = "EWI-26138, METIS-312668, IR-96983",
author = "Jorne Kandziora and Marieke Huisman and Christoph Bockisch and M. Zaharieva",
note = "10.1145/2786536.2786541",
year = "2015",
month = "7",
doi = "10.1145/2786536.2786541",
isbn = "978-1-4503-3656-7",
publisher = "Association for Computing Machinery (ACM)",
pages = "8",
editor = "R. Monahan",
booktitle = "Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs (FTfJP 2015)",
address = "United States",

}

Kandziora, J, Huisman, M, Bockisch, C & Zaharieva, M 2015, Run-time Assertion Checking of JML Annotations in Multithreaded Applications with e-OpenJML. in R Monahan (ed.), Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs (FTfJP 2015)., 8, Association for Computing Machinery (ACM), New York, pp. 8, 17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015, Prague, Czech Republic, 7-7 July. DOI: 10.1145/2786536.2786541

Run-time Assertion Checking of JML Annotations in Multithreaded Applications with e-OpenJML. / Kandziora, Jorne; Huisman, Marieke; Bockisch, Christoph; Zaharieva, M.

Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs (FTfJP 2015). ed. / R. Monahan. New York : Association for Computing Machinery (ACM), 2015. p. 8 8.

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

T1 - Run-time Assertion Checking of JML Annotations in Multithreaded Applications with e-OpenJML

AU - Kandziora,Jorne

AU - Huisman,Marieke

AU - Bockisch,Christoph

AU - Zaharieva,M.

N1 - 10.1145/2786536.2786541

PY - 2015/7

Y1 - 2015/7

N2 - Run-time assertion checking of multithreaded programs is challenging, as assertion evaluation should not interfere with the execution of other threads. This paper describes the prototype implementation of a run-time assertion checker that achieves this by evaluating assertions over snapshots of the state, instead of over the live state. Our prototype e-OpenJML, an extension to OpenJML, provides an easy to use, safe and interference-free evaluation of JML specifications in multithreaded programs. To achieve this, it integrates e-STROBE, our extension to the STROBE framework for asynchronous assertion evaluation. e-STROBE prevents all possible interferences between assertion evaluation and other program threads, which the original STROBE can not. It also simplifies evaluating assertions that relate the value of expressions in multiple states.

AB - Run-time assertion checking of multithreaded programs is challenging, as assertion evaluation should not interfere with the execution of other threads. This paper describes the prototype implementation of a run-time assertion checker that achieves this by evaluating assertions over snapshots of the state, instead of over the live state. Our prototype e-OpenJML, an extension to OpenJML, provides an easy to use, safe and interference-free evaluation of JML specifications in multithreaded programs. To achieve this, it integrates e-STROBE, our extension to the STROBE framework for asynchronous assertion evaluation. e-STROBE prevents all possible interferences between assertion evaluation and other program threads, which the original STROBE can not. It also simplifies evaluating assertions that relate the value of expressions in multiple states.

KW - EWI-26138

KW - METIS-312668

KW - IR-96983

U2 - 10.1145/2786536.2786541

DO - 10.1145/2786536.2786541

M3 - Conference contribution

SN - 978-1-4503-3656-7

SP - 8

BT - Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs (FTfJP 2015)

PB - Association for Computing Machinery (ACM)

ER -

Kandziora J, Huisman M, Bockisch C, Zaharieva M. Run-time Assertion Checking of JML Annotations in Multithreaded Applications with e-OpenJML. In Monahan R, editor, Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs (FTfJP 2015). New York: Association for Computing Machinery (ACM). 2015. p. 8. 8. Available from, DOI: 10.1145/2786536.2786541