Skip to main content
SpringerLink
Log in

Semantics for Locking Specifications

  • Conference paper
  • First Online:
NASA Formal Methods (NFM 2016)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9690))

Included in the following conference series:

Abstract

Lock-based synchronization disciplines, like Java’s @GuardedBy, are widely used to prevent concurrency errors. However, their semantics is often expressed informally and is consequently ambiguous. This article highlights such ambiguities and overcomes them by formalizing two possible semantics of @GuardedBy, using a reference operational semantics for a core calculus of a concurrent Java-like language. It also identifies when such annotations are actual guarantees against data races. Our work aids in understanding the annotations and supports the development of sound tools that verify or infer them.

Partially funded by Joint Project 2011 “Statical Analysis for Multithreading”.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Abadi, M., Flanagan, C., Freund, S.: Types for safe locking: static race detection for Java. ACM TOPLAS 28(2), 207–255 (2006)

    Article  Google Scholar 

  2. Ábrahám-Mumm, E., de Boer, F.S., de Roever, W.-P., Steffen, M.: Verification for java’s reentrant multithreading concept. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 5–20. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  3. Bandera: About Bandera. http://bandera.projects.cis.ksu.edu

  4. Bierman, G.M., Parkinson, M.J.: Effects and effect inference for a core java calculus. ENTCS 82(7), 82–107 (2003)

    Google Scholar 

  5. Blanchet, B.: Escape analysis for java: theory and practice. ACM TOPLAS 25(6), 713–775 (2003)

    Article  Google Scholar 

  6. Bogdanas, D., Rosu, G.: K-java: a complete semantics of java. In: ACM SIGPLAN-SIGACT POPL, pp. 445–456, Mumbai, India (2015)

    Google Scholar 

  7. Cenciarelli, P., Knapp, A., Reus, B., Wirsing, M.: From sequential to multi-threaded java: an event-based operational semantics. In: Johnson, M. (ed.) AMAST 1997. LNCS, vol. 1349, pp. 75–90. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  8. Dietl, W., Dietzel, S., Ernst, M.D., Muslu, K., Schiller, T.W.: Building and using pluggable type-checkers. In: Taylor, R.N., Gall, H.C. (eds.) ICSE 2011 (2011)

    Google Scholar 

  9. Ernst, M.D., Macedonio, D., Merro, M., Spoto, F.: Semantics for locking specifications. CoRR abs/1501.05338 (2015)

    Google Scholar 

  10. Ernst, M., Lovato, A., Macedonio, D., Spoto, F., Thaine, J.: Locking discipline inference and checking. In: ICSE 2016, Austin, TX, USA (2016)

    Google Scholar 

  11. Goetz, B., Peierls, T., Bloch, J., Bowbeer, J.: Java Concurrency in Practice. Addison Wesley, Boston (2006)

    Google Scholar 

  12. Google: Guava: Google Core Libraries for Java 1.6+. https://code.google.com/p/guava-libraries

  13. Hatcliff, J., Dwyer, M.B.: Using the bandera tool set to model-check properties of concurrent java software. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, p. 39. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  14. Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight java: a minimal core calculus for Java and GJ. ACM TOPLAS 23(3), 396–450 (2001)

    Article  Google Scholar 

  15. Javadoc for @GuardedBy. https://jsr-305.googlecode.com/svn/trunk/javadoc/javax/annotation/concurrent/GuardedBy.html

  16. Julia, S.: The Julia Static Analyzer. http://www.juliasoft.com/julia

  17. Long, B., Long, B.W.: Formal specification of java concurrency to assist software verification. In: Dongarra, J. (ed.) IPDPS 2003. IEEE Computer Society (2003)

    Google Scholar 

  18. NASA: Java PathFinder. http://babelfish.arc.nasa.gov/trac/jpf

  19. Nikolić, D.J., Spoto, F.: Definite expression aliasing analysis for java bytecode. In: Roychoudhury, A., D’Souza, M. (eds.) ICTAC 2012. LNCS, vol. 7521, pp. 74–89. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  20. Östlund, J., Wrigstad, T.: Welterweight java. In: Vitek, J. (ed.) TOOLS 2010. LNCS, vol. 6141, pp. 97–116. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  21. Palsberg, J., Schwartzbach, M.I.: Object-oriented type inference. In: Paepcke, A. (ed.) OOPSLA 1991, pp. 146–161. ACM SIGPLAN Notices, ACM, New York (1991)

    Google Scholar 

  22. Pech, V.: Concurrency is hot, try the JCIP annotations (2010). http://jetbrains.dzone.com/tips/concurrency-hot-try-jcip

Download references

Acknowledgments

We thank Ruggero Lanotte for valuable comments on an early draft. This material is based on research sponsored by DARPA under agreement numbers FA8750-12-2-0107, FA8750-15-C-0010, and FA8750-16-2-0032.

Author information

Authors and Affiliations

  1. Computer Science and Engineering, University of Washington, Seattle, WA, USA

    Michael D. Ernst

  2. Dipartimento di Informatica, Università degli Studi di Verona, Verona, Italy

    Damiano Macedonio, Massimo Merro & Fausto Spoto

Authors
  1. Michael D. Ernst
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Damiano Macedonio
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Massimo Merro
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Fausto Spoto
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Massimo Merro .

Editor information

Editors and Affiliations

  1. University of Minnesota, Minneapolis, Minnesota, USA

    Sanjai Rayadurgam

  2. NASA Ames Research Center , Moffett Field, California, USA

    Oksana Tkachuk

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Ernst, M.D., Macedonio, D., Merro, M., Spoto, F. (2016). Semantics for Locking Specifications. In: Rayadurgam, S., Tkachuk, O. (eds) NASA Formal Methods. NFM 2016. Lecture Notes in Computer Science(), vol 9690. Springer, Cham. https://doi.org/10.1007/978-3-319-40648-0_27

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-40648-0_27

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-40647-3

  • Online ISBN: 978-3-319-40648-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation