Run-time assertion checking of JML annotations in multithreaded applications with e-OpenJML

J. (Jorne) Kandziora; M. (Marieke) Huisman; C.M. Bockisch; M. (Marina) Zaharieva-Stojanovski

doi:10.1145/2786536.2786541

Run-time assertion checking of JML annotations in multithreaded applications with e-OpenJML

J. (Jorne) Kandziora, M. (Marieke) Huisman, C.M. Bockisch, M. (Marina) Zaharieva-Stojanovski

Research Program Learning and Innovation in Resilient systems (LIRS)

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

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 language	English
Title of host publication	FTfJP '15
Subtitle of host publication	Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs
Place of Publication	New York, NY
Publisher	Association for Computing Machinery (ACM)
Pages	1-6
Number of pages	6
ISBN (Print)	9781450336567
DOIs	https://doi.org/10.1145/2786536.2786541
Publication status	Published - Jul 2015
Event	European Conference on Object-Oriented Programming - Marriott Hotel, Prague, Czech Republic Duration: 5 Jul 2015 → 10 Jul 2015 Conference number: 29 https://2015.ecoop.org/

Conference

Conference	European Conference on Object-Oriented Programming
Abbreviated title	ECOOP 2015
Country/Territory	Czech Republic
City	Prague
Period	5/07/15 → 10/07/15
Internet address	https://2015.ecoop.org/

Access to Document

10.1145/2786536.2786541

Cite this

@inproceedings{a046e2daf0ae4f039d665efc14b2a902,

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.",

author = "Kandziora, {J. (Jorne)} and Huisman, {M. (Marieke)} and C.M. Bockisch and Zaharieva-Stojanovski, {M. (Marina)}",

year = "2015",

month = jul,

doi = "10.1145/2786536.2786541",

language = "English",

isbn = "9781450336567",

pages = "1--6",

booktitle = "FTfJP '15",

publisher = "Association for Computing Machinery (ACM)",

address = "United States",

note = "European Conference on Object-Oriented Programming, ECOOP 2015 ; Conference date: 05-07-2015 Through 10-07-2015",

url = "https://2015.ecoop.org/",

}

Kandziora, J, Huisman, M, Bockisch, CM & Zaharieva-Stojanovski, M 2015, Run-time assertion checking of JML annotations in multithreaded applications with e-OpenJML. in FTfJP '15: Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs., 8, Association for Computing Machinery (ACM), New York, NY, pp. 1-6, European Conference on Object-Oriented Programming, Prague, Czech Republic, 5/07/15. https://doi.org/10.1145/2786536.2786541

Run-time assertion checking of JML annotations in multithreaded applications with e-OpenJML. / Kandziora, J. (Jorne); Huisman, M. (Marieke); Bockisch, C.M. et al.

FTfJP '15: Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs. New York, NY : Association for Computing Machinery (ACM), 2015. p. 1-6 8.

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

TY - GEN

T1 - Run-time assertion checking of JML annotations in multithreaded applications with e-OpenJML

AU - Kandziora, J. (Jorne)

AU - Huisman, M. (Marieke)

AU - Bockisch, C.M.

AU - Zaharieva-Stojanovski, M. (Marina)

N1 - Conference code: 29

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.

U2 - 10.1145/2786536.2786541

DO - 10.1145/2786536.2786541

M3 - Conference Article in proceeding

SN - 9781450336567

SP - 1

EP - 6

BT - FTfJP '15

PB - Association for Computing Machinery (ACM)

CY - New York, NY

T2 - European Conference on Object-Oriented Programming

Y2 - 5 July 2015 through 10 July 2015

ER -

Run-time assertion checking of JML annotations in multithreaded applications with e-OpenJML

Abstract

Conference

Access to Document

Fingerprint

Cite this