Advertisement

Generation of Initial Contexts for Effective Deadlock Detection

  • Elvira Albert
  • Miguel Gómez-Zamalloa
  • Miguel Isabel
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10855)

Abstract

It has been recently proposed that testing based on symbolic execution can be used in conjunction with static deadlock analysis to define a deadlock detection framework that: (i) can show deadlock presence, in that case a concrete test-case and trace are obtained, and (ii) can also prove deadlock freedom. Such symbolic execution starts from an initial distributed context, i.e., a set of locations and their initial tasks. Considering all possibilities results in a combinatorial explosion on the different distributed contexts that must be considered. This paper proposes a technique to effectively generate initial contexts that can lead to deadlock, using the possible conflicting task interactions identified by static analysis, discarding other distributed contexts that cannot lead to deadlock. The proposed technique has been integrated in the above-mentioned deadlock detection framework hence enabling it to analyze systems without the need of any user supplied initial context.

References

  1. 1.
    Agarwal, R., Wang, L., Stoller, S.D.: Detecting potential deadlocks with static analysis and run-time monitoring. In: Ur, S., Bin, E., Wolfsthal, Y. (eds.) HVC 2005. LNCS, vol. 3875, pp. 191–207. Springer, Heidelberg (2006).  https://doi.org/10.1007/11678779_14CrossRefGoogle Scholar
  2. 2.
    Albert, E., Gómez-Zamalloa, M., Isabel, M.: Deadlock Guided Testing in CLP. Technical report (2017). http://costa.ls.fi.upm.es/papers/costa/AlbertGI17tr.pdf
  3. 3.
    Albert, E., Gómez-Zamalloa, M., Isabel, M.: Combining static analysis and testing for deadlock detection. In: Ábrahám, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 409–424. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-33693-0_26CrossRefGoogle Scholar
  4. 4.
    Albert, E., Gómez-Zamalloa, M., Isabel, M.: SYCO: a systematic testing tool for concurrent objects. In: Proceedings of CC 2016. ACM (2016)Google Scholar
  5. 5.
    Albert, E., Gómez-Zamalloa, M., Isabel, M.: On the generation of initial contexts for effective deadlock detection. Technical report, October 2017. https://arxiv.org/abs/1709.04255
  6. 6.
    Christakis, M., Gotovos, A., Sagonas, K.F.: Systematic testing for detecting concurrency errors in erlang programs. In: Sixth IEEE International Conference on Software Testing, Verification and Validation, ICST 2013, Luxembourg, Luxembourg, 18–22 March 2013. IEEE Computer Society (2013)Google Scholar
  7. 7.
    de Boer, F.S., Clarke, D., Johnsen, E.B.: A complete guide to the future. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 316–330. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-71316-6_22CrossRefGoogle Scholar
  8. 8.
    Flanagan, C., Felleisen, M.: The semantics of future and its use in program optimization. In: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (1995)Google Scholar
  9. 9.
    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
  10. 10.
    Giachino, E., Grazia, C.A., Laneve, C., Lienhardt, M., Wong, P.Y.H.: Deadlock analysis of concurrent objects: theory and practice. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 394–411. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-38613-8_27CrossRefGoogle Scholar
  11. 11.
    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
  12. 12.
    Laneve, C., Giachino, E., Lienhardt, M.: A framework for deadlock detection in core ABS. Softw. Syst. Model. 15(4), 1013–1048 (2016)CrossRefGoogle Scholar
  13. 13.
    Johnsen, E.B., Hähnle, R., Schäfer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 142–164. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-25271-6_8CrossRefGoogle Scholar
  14. 14.
    Joshi, P., Naik, M., Sen, K., Gay, D.: An effective dynamic analysis for detecting generalized deadlocks. In: Proceedings of FSE 2010. ACM (2010)Google Scholar
  15. 15.
    Joshi, P., Park, C., Sen, K., Naik, M.: A randomized dynamic program analysis technique for detecting real deadlocks. In: Proceedings of PLDI 2009. ACM (2009)Google Scholar
  16. 16.
    Kheradmand, A., Kasikci, B., Candea, G.: Lockout: Efficient Testing for Deadlock Bugs. Technical report (2013). http://dslab.epfl.ch/pubs/lockout.pdf
  17. 17.
    Masticola, S.P., Ryder, B.G.: A model of Ada programs for static deadlock detection in polynomial time. In: Parallel and Distributed Debugging, pp. 97–107. ACM (1991)Google Scholar
  18. 18.
    Milanova, A., Rountev, A., Ryder, B.G.: Parameterized object sensitivity for points-to analysis for java. ACM Trans. Softw. Eng. Methodol. 14, 1–41 (2005)CrossRefGoogle Scholar
  19. 19.
    Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.E.: Eraser: a dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst. 15(4), 391–411 (1997)CrossRefGoogle Scholar
  20. 20.
    Sen, K., Agha, G.: Automated systematic testing of open distributed programs. In: Baresi, L., Heckel, R. (eds.) FASE 2006. LNCS, vol. 3922, pp. 339–356. Springer, Heidelberg (2006).  https://doi.org/10.1007/11693017_25CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Elvira Albert
    • 1
  • Miguel Gómez-Zamalloa
    • 1
  • Miguel Isabel
    • 1
  1. 1.Complutense University of Madrid (UCM)MadridSpain

Personalised recommendations