Skip to main content
SpringerLink
Log in

Deadlock Detection of Java Bytecode

  • Conference paper
  • First Online:
Logic-Based Program Synthesis and Transformation (LOPSTR 2017)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10855))

Abstract

This paper presents a technique for deadlock detection of Java programs. The technique uses typing rules for extracting infinite-state abstract models of the dependencies among the components of the Java intermediate language – the Java bytecode. Models are subsequently analysed by means of an extension of a solver that we have defined for detecting deadlocks in process calculi. Our technique is complemented by a prototype verifier that also covers most of the Java features.

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 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Notes

  1. 1.

    http://bugs.java.com/.

  2. 2.

    https://issues.apache.org/jira.

  3. 3.

    The technical details of type safety appear in [12].

  4. 4.

    Actually, has a minor difference with respect to : in , local variables are addressed by non-negative integers instead of names.

  5. 5.

    http://www.contemplateltd.com/threadsafe.

  6. 6.

    https://github.com/abelunibo/Java-Deadlocks.

References

  1. Atkey, R., Sannella, D.: ThreadSafe: static analysis for Java concurrency. In: ECEASST, vol. 72 (2015). http://journal.ub.tu-berlin.de/eceasst/article/view/1025

  2. Bensalem, S., Havelund, K.: Dynamic deadlock analysis of multi-threaded programs. In: Ur, S., Bin, E., Wolfsthal, Y. (eds.) HVC 2005. LNCS, vol. 3875, pp. 208–223. Springer, Heidelberg (2006). https://doi.org/10.1007/11678779_15

    Chapter  Google Scholar 

  3. Eslamimehr, M., Palsberg, J.: Sherlock: scalable deadlock detection for concurrent programs. In Proceedings of the 22nd International Symposium on Foundations of Software Engineering (FSE-22), pp. 353–365. ACM (2014)

    Google Scholar 

  4. Ferrara, P.: Checkmate: a generic static analyzer of java multithreaded programs. In: Proceedings of 7th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2009, pp. 169–178. IEEE Computer Society (2009)

    Google Scholar 

  5. Flores-Montoya, A.E., Albert, E., Genaim, S.: May-happen-in-parallel based deadlock analysis for concurrent objects. In: Beyer, D., Boreale, M. (eds.) FMOODS/FORTE -2013. LNCS, vol. 7892, pp. 273–288. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38592-6_19

    Chapter  Google Scholar 

  6. Garcia, A.: Static analysis of concurrent programs based on behavioral type systems. Ph.D. thesis, School in Computer Science and Engineering (2017). JaDA.cs.unibo.it

  7. Giachino, E., Kobayashi, N., Laneve, C.: Deadlock analysis of unbounded process networks. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 63–77. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44584-6_6

    Chapter  Google Scholar 

  8. Giachino, E., Laneve, C.: Deadlock detection in linear recursive programs. In: Bernardo, M., Damiani, F., Hähnle, R., Johnsen, E.B., Schaefer, I. (eds.) SFM 2014. LNCS, vol. 8483, pp. 26–64. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-07317-0_2

    Chapter  Google Scholar 

  9. Giachino, E., Laneve, C., Lienhardt, M.: A framework for deadlock detection in core ABS. Softw. Syst. Model. 15(4), 1013–1048 (2016)

    Article  Google Scholar 

  10. Kobayashi, N., Laneve, C.: Deadlock analysis of unbounded process networks. Inf. Comput. 252, 48–70 (2017)

    Article  MathSciNet  Google Scholar 

  11. Laneve, C.: A lightweight deadlock analysis technique of object-oriented programs, January 2018. Submitted for publication

    Google Scholar 

  12. Laneve, C., Garcia, A.: Deadlock detection of Java Bytecode (full version), November 2017. cs.unibo.it/~laneve/papers/ddJB.pdf

  13. Naik, M., Park, C.-S., Sen, K., Gay, D.: Effective static deadlock detection. In: 31st International Conference on Software Engineering (ICSE 2009), pp. 386–396. ACM (2009)

    Google Scholar 

  14. Odersky, M., et al.: An overview of the scala programming language. Technical report IC/2004/64, EPFL, Lausanne, Switzerland (2004)

    Google Scholar 

Download references

Acknowledgments

We thank Elena Giachino for the fruitful discussions and useful comments, in particular for the help in the proof of Theorem 2.

Author information

Authors and Affiliations

  1. Department of Computer Science and Engineering, University of Bologna – Inria Focus, Bologna, Italy

    Cosimo Laneve & Abel Garcia

Authors
  1. Cosimo Laneve
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Abel Garcia
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Cosimo Laneve .

Editor information

Editors and Affiliations

  1. University of Chieti-Pescara, Pescara, Italy

    Fabio Fioravanti

  2. Roskilde University, Roskilde, Denmark

    John P. Gallagher

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Laneve, C., Garcia, A. (2018). Deadlock Detection of Java Bytecode. In: Fioravanti, F., Gallagher, J. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2017. Lecture Notes in Computer Science(), vol 10855. Springer, Cham. https://doi.org/10.1007/978-3-319-94460-9_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-94460-9_3

  • Published:

  • Publisher Name: Springer, Cham

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

  • Online ISBN: 978-3-319-94460-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation