Advertisement

Deadlock Detection of Java Bytecode

  • Cosimo Laneve
  • Abel Garcia
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, 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.

Notes

Acknowledgments

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

References

  1. 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. 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_15CrossRefGoogle Scholar
  3. 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. 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. 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_19CrossRefGoogle Scholar
  6. 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. 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_6CrossRefGoogle Scholar
  8. 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_2CrossRefGoogle Scholar
  9. 9.
    Giachino, E., Laneve, C., Lienhardt, M.: A framework for deadlock detection in core ABS. Softw. Syst. Model. 15(4), 1013–1048 (2016)CrossRefGoogle Scholar
  10. 10.
    Kobayashi, N., Laneve, C.: Deadlock analysis of unbounded process networks. Inf. Comput. 252, 48–70 (2017)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Laneve, C.: A lightweight deadlock analysis technique of object-oriented programs, January 2018. Submitted for publicationGoogle Scholar
  12. 12.
    Laneve, C., Garcia, A.: Deadlock detection of Java Bytecode (full version), November 2017. cs.unibo.it/~laneve/papers/ddJB.pdf
  13. 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. 14.
    Odersky, M., et al.: An overview of the scala programming language. Technical report IC/2004/64, EPFL, Lausanne, Switzerland (2004)Google Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Department of Computer Science and EngineeringUniversity of Bologna – Inria FocusBolognaItaly

Personalised recommendations