skip to main content
10.1145/2786536.2786541acmotherconferencesArticle/Chapter ViewAbstractPublication PagesisstaConference Proceedingsconference-collections
research-article

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

Published: 07 July 2015 Publication History

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.

References

[1]
E. E. Aftandilian, S. Z. Guyer, M. Vechev, and E. Yahav. Asynchronous assertions. In OOPSLA '11, pages 275--288. ACM Press, 2011.
[2]
B. Alpern, S. Augart, S. M. Blackburn, M. Butrico, A. Cocchi, P. Cheng, J. Dolby, S. Fink, D. Grove, M. Hind, K. S. McKinley, M. Mergen, J. E. B. Moss, T. Ngo, V. Sarkar, and M. Trapp. The Jikes Research Virtual Machine project: Building an open-source research community. IBM Systems Journal, 44(2):399--417, 2005.
[3]
A. Amighi, S. Blom, S. Darabi, M. Huisman, W. Mostowski, and M. Zaharieva-Stojanovski. Verification of concurrent systems with VerCors. In SFM-14:ESM, volume 8483 of LNCS, pages 172--216. Springer, 2014.
[4]
W. Araujo, L. C. Briand, and Y. Labiche. Enabling the runtime assertion checking of concurrent contracts for the Java modeling language. In ICSE '11, page 786. ACM Press, 2011.
[5]
S. Blackburn, R. Garner, and D. Frampton. MMTk: The Memory Management Toolkit, 2006.
[6]
R. Bornat, C. Calcagno, P. O'Hearn, and M. Parkinson. Permission accounting in separation logic. In POPL'05, pages 259--270. ACM, 2005.
[7]
L. Burdy, Y. Cheon, D. R. Cok, M. D. Ernst, J. R. Kiniry, G. T. Leavens, K. R. M. Leino, and E. Poll. An overview of JML tools and applications. STTT, 7(3):212--232, June 2005.
[8]
Y. Cheon. A Runtime Assertion Checker for the Java Modeling Language. PhD thesis, Department of Computer Science, Iowa State University, Ames, 2003.
[9]
Y. Cheon and G. T. Leavens. A Runtime Assertion Checker for the Java Modeling Language. In International Conference on Software Engineering Research and Practice, pages 322--328, 2002.
[10]
D. R. Cok. OpenJML: JML for Java 7 by Extending OpenJDK. In NFM'11, pages 472--479, Berlin, Heidelberg, 2011. Springer.
[11]
D. R. Cok. OpenJML User Guide, 2013.
[12]
D. R. Cok and G. T. Leavens. Extensions of the theory of observational purity and a practical design for JML. In SAVCBS 2008, pages 43--50, 2008.
[13]
C. P. T. de Gouw and F. S. de Boer. Run-time verification of black-box components using behavioral specifications: An experience report on tool development. In FACS2012, volume 7684 of LNCS, pages 128--133. Springer, 2013.
[14]
C. P. T. de Gouw, F. S. de Boer, and J. J. Vinju. Prototyping a tool environment for run-time assertion checking in JML with communication histories. In FTfJP 2010. ACM, 2010.
[15]
R. H. Halstead, Jr. MULTILISP: A Language for Concurrent Symbolic Computation. ACM Trans. Program. Lang. Syst., 7(4):501--538, Oct. 1985.
[16]
P. Joshi, M. Naik, C.-S. Park, and K. Sen. CalFuzzer: An extensible active testing framework for concurrent programs. In CAV '09, pages 675--681. Springer, 2009.
[17]
D. Lea. JSR166: Concurrency Utilities. https://www.jcp.org/en/jsr/detail?id=166, 2004.
[18]
G. T. Leavens, A. L. Baker, and C. Ruby. Preliminary design of JML: a behavioral interface specification language for java. SIGSOFT Softw Eng Notes, 31(3):1--38, 2006.
[19]
H. Rebêlo, G. T. Leavens, M. Bagherzadeh, H. Rajan, R. Lima, D. Zimmerman, M. Cornélio, and T. Thüm. AspectJML: Modular specification and runtime checking for crosscutting contracts. In Modularity 2014, 2014.
[20]
E. Rodriguez, M. Dwyer, C. Flanagan, J. Hatcliff, G. T. Leavens, and Robby. Extending JML for modular specification and verification of multi-threaded programs. In ECOOP 2005, pages 551--576. Springer, 2005.
[21]
F. Schneider. Enforceable security policies. Technical Report TR99-1759, Cornell University, October 1999.
[22]
A. Welc, S. Jagannathan, and A. Hosking. Safe futures for Java. In ACM SIGPLAN Notices, volume 40, pages 439--453. ACM, 2005.

Cited By

View all
  • (2021)The e-ACSL perspective on runtime assertion checkingProceedings of the 5th ACM International Workshop on Verification and mOnitoring at Runtime EXecution10.1145/3464974.3468451(8-12)Online publication date: 12-Jul-2021
  • (2016)Run-Time Checking Multi-threaded Java ProgramsProceedings of the 42nd International Conference on SOFSEM 2016: Theory and Practice of Computer Science - Volume 958710.1007/978-3-662-49192-8_18(217-228)Online publication date: 23-Jan-2016

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Other conferences
FTfJP '15: Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs
July 2015
49 pages
ISBN:9781450336567
DOI:10.1145/2786536
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 July 2015

Permissions

Request permissions for this article.

Check for updates

Qualifiers

  • Research-article

Funding Sources

  • ERC

Conference

ECOOP '15

Acceptance Rates

FTfJP '15 Paper Acceptance Rate 9 of 14 submissions, 64%;
Overall Acceptance Rate 51 of 75 submissions, 68%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)2
  • Downloads (Last 6 weeks)0
Reflects downloads up to 09 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2021)The e-ACSL perspective on runtime assertion checkingProceedings of the 5th ACM International Workshop on Verification and mOnitoring at Runtime EXecution10.1145/3464974.3468451(8-12)Online publication date: 12-Jul-2021
  • (2016)Run-Time Checking Multi-threaded Java ProgramsProceedings of the 42nd International Conference on SOFSEM 2016: Theory and Practice of Computer Science - Volume 958710.1007/978-3-662-49192-8_18(217-228)Online publication date: 23-Jan-2016

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media