Related Work on Deadlock and Termination Detection Techniques

  • Wiktor B. DaszczukEmail author
Part of the Studies in Computational Intelligence book series (SCI, volume 817)


Because many deadlock detection techniques evolved, even the concept of deadlock varies across papers.


  1. Agarwal, R., & Stoller, S. D. (2006). Run-time detection of potential deadlocks for programs with locks, semaphores, and condition variables. In Proceedings of the Workshop on Parallel and Distributed Systems: Testing and Debugging (PADTAD-IV), ISSTA, 2006, Portland, ME, 17–20 July 2006 (pp. 51–59). New York, NY: ACM.
  2. Allen, G. E., Zucknick, P. E., & Evans, B. L. (2007). A distributed deadlock detection and resolution algorithm for process networks. In 2007 IEEE International Conference on Acoustics, Speech and Signal Processing—ICASSP ’07, 15–20 April 2007, Honolulu, HI (Vol.2, pp. II-33–II-36). New York, NY: IEEE.
  3. Arcaini, P., Gargantini, A., & Riccobene, E. (2009). AsmetaSMV: A model checker for AsmetaL models—Tutorial. Url:
  4. Arcile, J., Czachórski, T., … Rataj, A. (2016). Modelling and analysing mixed reality applications. In A. Gruca, A. Brachman, S. Kozielski, & T. Czachórski (Eds.), Man-Machine Interactions 4: 4th International Conference on Man-Machine Interactions, ICMMI 2015 Kocierz Pass, Poland, 6–9 Oct. 2015 (pp. 3–17). Cham, Switzerland: Springer International Publishing.
  5. Attie, P. C. (2016). Synthesis of large dynamic concurrent programs from dynamic specifications. Formal Methods in System Design, 47(131), 1–54. Scholar
  6. Baier, C., & Katoen, J.-P. (2008). Principles of model checking. Cambridge, MA: MIT Press. ISBN: 9780262026499.zbMATHGoogle Scholar
  7. Beneš, N., Černá, I., … Zimmerova, B. (2008). A case study in parallel verification of component-based systems. Electronic Notes in Theoretical Computer Science, 220(2), 67–83.
  8. Bensalem, S., Griesmayer, A., … Peled, D. (2011). Efficient deadlock detection for concurrent systems. In 9th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2011, Cambridge, UK, 11–13 July 2011 (pp. 119–129). New York, NY: IEEE.
  9. Bérard, B., Bidoit, M., … Schnoebelen, P. (2001). Systems and software verification. Model-checking techniques and tools. Heidelberg: Springer. ISBN: 978-3-642-07478-3,
  10. Bertino, E., Chiola, G., & Mancini, L. V. (1998). Deadlock detection in the face of transaction and data dependencies. In 19th International Conference ICATPN’98, Lisbon, Portugal, 22–26 June 1998 (pp. 266–285). Heidelberg: Springer.
  11. Chalopin, J., Godard, E., … Tel, G. (2007). About the termination detection in the asynchronous message passing model. In 33rd Conference on Current Trends in Theory and Practice of Computer Science, Harrachov, Czech Republic, 20–26 Jan. 2007 (pp. 200–211). Heidelberg: Springer.
  12. Chandy, K. M., & Lamport, L. (1985). Distributed snapshots: Determining global states of distributed systems. ACM Transactions on Computer Systems, 3(1), 63–75. Scholar
  13. Chandy, K. M., Misra, J., & Haas, L. M. (1983). Distributed deadlock detection. ACM Transactions on Computer Systems, 1(2), 144–156. Scholar
  14. Chang, F. S.-H., & Jackson, D. (2006). Symbolic model checking of declarative relational models. In Proceeding of the 28th International Conference on Software Engineering—ICSE ’06, Shanghai, China, 20–28 May 2006 (pp. 312–320). New York, USA: ACM Press.
  15. Cho, J., Yoo, J., & Cha, S. (2006). NuEditor—A tool suite for specification and verification of NuSCR. In SERA 2004: Software Engineering Research and Applications, Los Angeles, CA, 5–7 May 2004, LNCS Vol. 3647 (pp. 19–28). Heidelberg: Springer.
  16. Choudhary, A. N., Kohler, W. H., … Towsley, D. (1989). A modified priority based probe algorithm for distributed deadlock detection and resolution. IEEE Transactions on Software Engineering, 15(1), 10–17.
  17. Chu, F., & Xie, X.-L. (1997). Deadlock analysis of Petri nets using siphons and mathematical programming. IEEE Transactions on Robotics and Automation, 13(6), 793–804. Scholar
  18. Clarke, E. M., Grumberg, O., & Peled, D. (1999). Model checking. Cambridge, MA: MIT Press. ISBN: 0-262-03270-8.Google Scholar
  19. Coffman, E. G., Elphick, M., & Shoshani, A. (1971). System deadlocks. ACM Computing Surveys, 3(2), 67–78. Scholar
  20. Corbett, J. C. (1994). An empirical evaluation of three methods for deadlock analysis of Ada tasking programs. In Proceedings of the 1994 International Symposium on Software Testing and Analysis—ISSTA ’94,), Seattle, WA, 17–19 Aug. 1994 (pp. 204–215). New York, NY: ACM Press.
  21. Corbett, J. C. (1996). Evaluating deadlock detection methods for concurrent software. IEEE Transactions on Software Engineering, 22(3), 161–180. Scholar
  22. Cordeiro, L. (2010). SMT-based bounded model checking for multi-threaded software in embedded systems. In Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering—ICSE ’10, Cape Town, RSA, 2–8 May 2010 (Vol. 2, pp. 373–376). New York, NY: ACM Press.
  23. Craig, D. C., & Zuberek, W. M. (2008). Two-stage siphon-based deadlock detection in Petri nets. In P. Petratos & P. Dandapami (Eds.), Current advances in computing, engineering and information technology (pp. 317–330). Palermo, Italy: Int. Society for Advanced Research.Google Scholar
  24. Daszczuk, W. B. (2003). Verification of temporal properties in concurrent systems. Warsaw University of Technology. Url:
  25. De Francesco, N., Santone, A., & Vaglini, G. (1998). State space reduction by non-standard semantics for deadlock analysis. Science of Computer Programming, 30(3), 309–338. Scholar
  26. Dijkstra, E. W., & Scholten, C. S. (1980). Termination detection for diffusing computations. Information Processing Letters, 11(1), 1–4. Scholar
  27. Duri, S., Buy, U., … Shatz, S. M. (1994). Application and experimental evaluation of state space reduction methods for deadlock analysis in Ada. ACM Transactions on Software Engineering and Methodology, 3(4), 340–380.
  28. Elmagarmid, A. K. (1986). A survey of distributed deadlock detection algorithms. ACM SIGMOD Record, 15(3), 37–45. Scholar
  29. Fahland, D., Favre, C., … Wolf, K. (2011). Analysis on demand: Instantaneous soundness checking of industrial business process models. Data & Knowledge Engineering, 70(5), 448–466.
  30. Garanina, N. O., & Bodin, E. V. (2014). Distributed termination detection by counting agent. In 23th International Workshop on Concurrency, Specification and Programming, CS&P, Chemnitz, Germany, 29 Sept.–1 Oct. 2014 (pp. 69–79). Berlin, Germany: Humboldt University. Url:
  31. Geilen, M., & Basten, T. (2003). Requirements on the execution of Kahn process networks. In ESOP’03 the 12th European Symposium on Programming, Warsaw, Poland, 7–11 April 2003, LNCS 2618 (pp. 319–334). Heidelberg: Springer.
  32. Gerth, R., Kuiper, R., … Szreter, M. (1999). Partial order reductions preserving simulations. In Concurrency Specification and Programming (CS&P), Warsaw, Poland, 28–30 Sept. 1999 (pp. 153–171). Url:
  33. Godefroid, P., & Wolper, P. (1992). Using partial orders for the efficient verification of deadlock freedom and safety properties. In 3rd International Workshop, CAV ’91, Aalborg, Denmark, 1–4 July, 1991, LNCS 575 (pp. 332–342). Heidelberg: Springer.
  34. Grover, H., & Kumar, S. (2013). Analysis of deadlock detection and resolution techniques in distributed database environment. International Journal of Computer Engineering & Science, 2(1), 17–25. Url:
  35. Guan, X., Li, Y., … Wang, S. (2012). A literature review of deadlock prevention policy based on petri nets for automated manufacturing systems. International Journal of Digital Content Technology and Its Applications, 6(21), 426–433.
  36. Havelund, K., & Pressburger, T. (2000). Model checking JAVA programs using JAVA PathFinder. International Journal on Software Tools for Technology Transfer (STTT), 2(4), 366–381. Scholar
  37. Havelund, K., & Skakkebæk, J. U. (1999). Applying model checking in java verification. In 5th and 6th International SPIN Workshops, Trento, Italy, July 5, 1999, Toulouse, France, 21 and 24 Sept. 1999 (pp. 216–231). London, UK: Springer.
  38. Heußner, A., Poskitt, C. M., … Morandi, B. (2015). Towards practical graph-based verification for an object-oriented concurrency model. Electronic Proceedings in Theoretical Computer Science, 181, 32–47.
  39. Hilbrich, T., de Supinski, B. R., … Müller, M. S. (2009). A graph based approach for MPI deadlock detection. In Proceedings of the 23rd International Conference on Supercomputing—ICS ’09, Yorktown Heights, NY, 8–12 June 2009 (pp. 296–305). New York, NY: ACM Press.
  40. Hilbrich, T., de Supinski, B. R., … Müller, M. S. (2013). Distributed wait state tracking for runtime MPI deadlock detection. In Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis on SC ’13, Denver, CO, 17–21 Nov. 2013 (pp. 1–12). New York: ACM Press.
  41. Hiraishi, H. (2000). Verification of deadlock free property of high level robot control. In Proceedings of the Ninth Asian Test Symposium ATS 2000, Taipei, 4–6 Dec. 2000 (pp. 198–203). New York, NY: IEEE Comput. Soc.
  42. Holt, R. C. (1972). Some deadlock properties of computer systems. ACM Computing Surveys, 4(3), 179–196. Scholar
  43. Holzmann, G. J. (1995). Tutorial: Proving properties of concurrent systems with SPIN. In 6th International Conference on Concurrency Theory, CONCUR’95, Philadelphia, PA, 21–24 Aug. 1995 (pp. 453–455). Heidelberg: Springer.
  44. Holzmann, G. J. (1997). The model checker SPIN. IEEE Transactions on Software Engineering, 23(5), 279–295. Scholar
  45. Hosseini, R., & Haghighat, A. T. (2005). An improved algorithm for deadlock detection and resolution in mobile agent systems. In International Conference on Computational Intelligence for Modelling, Control and Automation and International Conference on Intelligent Agents, Web Technologies and Internet Commerce (CIMCA-IAWTIC’06), Vienna, Austria, 28–30 Nov. 2005, (Vol. 2, pp. 1037–1042). New York, NY: IEEE.
  46. Huang, S.-T. (1989). Detecting termination of distributed computations by external agents. In [1989] Proceedings. The 9th International Conference on Distributed Computing Systems, Newport Beach, CA, 5–9 June 1989 (pp. 79–84). New York, NY: IEEE Comput. Soc. Press.
  47. Inverso, O., Nguyen, T. L., … Parlato, G. (2015). Lazy-CSeq: A context-bounded model checking tool for multi-threaded C-programs. In 2015 30th IEEE/ACM International Conference on Automated Software Engineering (ASE), Lincoln, NE, 9–13 Nov. 2015 (pp. 807–812). New York, NY: IEEE.
  48. Isloor, S. S., & Marsland, T. A. (1980). The deadlock problem: An overview. Computer, 13(9), 58–78. Scholar
  49. Joosten, S. J. C., Julien, F. V., & Schmaltz, J. (2014). WickedXmas: Designing and verifying on-chip communication fabrics. In 3rd International Workshop on Design and Implementation of Formal Tools and Systems, DIFTS’14, Lausanne, Switzerland, 20 Oct. 2014 (pp. 1–8). Eindhoven, The Netherlands: Technische Universiteit Eindhoven. Url:
  50. Karacali, B., Tai, K.-C., & Vouk, M. A. (2000). Deadlock detection of EFSMs using simultaneous reachability analysis. In Proceeding International Conference on Dependable Systems and Networks. DSN 2000, New York, NY, 25–28 June 2000 (pp. 315–324). New York, NY: IEEE Comput. Soc.
  51. Karatkevich, A., & Grobelna, I. (2014). Deadlock detection in Petri nets: One trace for one deadlock? In 2014 7th International Conference on Human System Interactions (HSI), Costa da Caparica, Lisbon, Portugal, 16–18 June 2014 (pp. 227–231). New York, NY: IEEE.
  52. Kaveh, N. (2001). Using model checking to detect deadlocks in distributed object systems. In W. Emmerich & S. Tai (Eds.), 2nd International Workshop on Distributed Objects, Davis, CA, 2–3 Nov. 2000, LNCS vol. 1999 (pp. 116–128). London, UK: Springer.
  53. Kaveh, N., & Emmerich, W. (2001). Deadlock detection in distribution object systems. In Proceedings of the 8th European Software Engineering Conference held Jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering—ESEC/FSE-9, Vienna, Austria, 10–14 Sept. 2001 (pp. 44–51). New York, NY: ACM Press.
  54. Kern, C., & Greenstreet, M. R. (1999). Formal verification in hardware design: A survey. ACM Transactions on Design Automation of Electronic Systems, 4(2), 123–193. Scholar
  55. Knapp, E. (1987). Deadlock detection in distributed databases. ACM Computing Surveys, 19(4), 303–328. Scholar
  56. Kokash, N., & Arbab, F. (2008). Formal behavioral modeling and compliance analysis for service-oriented systems. In F. S. de Boer (Ed.), Formal Methods for Components and Objects - 7th International Symposium, FMCO 2008, Sophia Antipolis, France, 21–23 Oct. 2008, LNCS 5751 (pp. 21–41). Heidelberg: Springer.
  57. Kshemkalyani, A. D., & Mukesh, S. (2008). Distributed computing. Principles, algorithms, and systems. Cambridge, UK: Cambridge University Press. ISBN: 978-0-521-87634-6.Google Scholar
  58. Kumar, D. (1985). A class of termination detection algorithms for distributed computations. In Fifth Conference on Foundations of Software Technology and Theoretical Computer Science, New Delhi, India 16–18 Dec. 1985 (pp. 73–100). Heidelberg: Springer.
  59. Leibfried, T. F. (1989). A deadlock detection and recovery algorithm using the formalism of a directed graph matrix. ACM SIGOPS Operating Systems Review, 23(2), 45–55. Scholar
  60. Li, T., Ellis, C. S., … Sorin, D. J. (2005). Pulse : A dynamic deadlock detection mechanism using speculative execution. In USENIX Annual Technical Conference, Anaheim, CA, 10–15 April 2005 (pp. 31–44). Berkeley, CA: USENIX Association. Url:
  61. Longley, D., & Shain, M. (1986). Dictionary of information technology. London: Macmillan Press. ISBN: 0-19-520519-7.Google Scholar
  62. Ma, G. (2007). Model checking support for CoreASM: Model checking distributed abstract state machines using Spin, MSc Thesis. Simon Fraser University, Burnaby, Canada. Url:
  63. Magee, J., & Kramer, J. (1999). Concurrency: Models and programs—From finite state models to java programs. Chichester: Wiley. ISBN: 0470093552.zbMATHGoogle Scholar
  64. Martens, M. (2009). Establishing properties of interaction systems, PhD Thesis. University of Mannheim. Url:
  65. Masticola, S. P., & Ryder, B. G. (1990). Static infinite wait anomaly detection in polynomial time. In 1990 International Conference on Parallel Processing, Urbana-Champaign, IL, 13–17 Aug. 1990 (Vol. 2, pp. 78–87). University Park, PA: Pennsylvania State University Press. Url:
  66. Matocha, J., & Camp, T. (1998). A taxonomy of distributed termination detection algorithms. Journal of Systems and Software, 43(3), 207–221. Scholar
  67. Mattern, F. (1987). Algorithms for distributed termination detection. Distributed Computing, 2(3), 161–175. Scholar
  68. Mattern, F. (1989). Global quiescence detection based on credit distribution and recovery. Information Processing Letters, 30(4), 195–200. Scholar
  69. Mazuelo, C. L. (2008). Automatic model checking of UML models. Universitat Berlin. Url:
  70. Milner, R. (1984). A calculus of communicating systems. Heidelberg: Springer LNCS vol. 92, Scholar
  71. Mitchell, D. P., & Merritt, M. J. (1984). A distributed algorithm for deadlock detection and resolution. In Proceedings of the Third Annual ACM Symposium on Principles of Distributed Computing—PODC ’84, Vancouver, Canada, 27–29 Aug. 1984 (pp. 282–284). New York, NY: ACM Press.
  72. Natarajan, N. (1986). A distributed scheme for detecting communication deadlocks. IEEE Transactions on Software Engineering, SE-12(4), 531–537.
  73. Nguyen, H. H. C., Le, V. S., & Nguyen, T. T. (2014). Algorithmic approach to deadlock detection for resource allocation in heterogeneous platforms. In 2014 International Conference on Smart Computing, Hong Kong, 3–5 Nov. 2014 (pp. 97–103). New York, NY: IEEE.
  74. Ni, Q., Sun, W., & Ma, S. (2009). Deadlock detection based on resource allocation graph. In 2009 Fifth International Conference on Information Assurance and Security, Xian, China, 18–20 Aug. 2009 (pp. 135–138). IEEE.
  75. Olson, A. G., & Evans, B. L. (2005). Deadlock detection for distributed process networks. In ICASSP ’05. IEEE International Conference on Acoustics, Speech, and Signal Processing, Philadelphia, PA, 18–23 March 2005 (Vol. 5, pp. 73–76). New York, NY: IEEE.
  76. Park, Y. C., & Scheuermann, P. (1991). A deadlock detection and resolution algorithm for sequential transaction processing with multiple lock modes. In 1991 The Fifteenth Annual International Computer Software & Applications Conference, Tokyo, Japan, 11–13 Sept. 1991 (pp. 70–77). New York, NY: IEEE Comput. Soc. Press.
  77. Penczek, W., Szreter, M., … Kuiper, R. (2000). Improving partial order reductions for universal branching time properties. Fundamenta Informaticae, 43(1–4), 245–267.
  78. Peri, S., & Mittal, N. (2004). On termination detection in an asynchronous distributed system. In 17th ISCA International Conference on Parallel and Distributed Computing Systems (PDCS), San Francisco, CA, 15–17 Sept. 2004 (pp. 209–215). Url:
  79. Perna, J., & George, C. (2006). Model checking RAISE specifications. Url:
  80. Petrovic, T., Bogdan, S., & Sindicic, I. (2009). Determination of circular waits in multiple-reentrant flowlines based on machine-job incidence matrix. In European Control Conference (ECC) 2009, Budapest, Hungary, 23–26 Aug. 2009 (pp. 4463–4468). New York, NY: IEEE. DOI:
  81. Podelski, A., & Rybalchenko, A. (2003). Software model checking of liveness properties via transition invariants, Research Report MPI–I–2003–2–00, Max Planck Institite fur Informatik, December 2003. Url:
  82. Puhakka, A., & Valmari, A. (2000). Livelocks, fairness and protocol verification. In 16th World Conference on Software: Theory and Practice, Beijing, China, 21–25 Aug. 2000, IFIP (pp. 471–479). Laxenburg, Austria: International Federation for Information Processing. Url:
  83. Ray, I., & Ray, I. (2001). Detecting termination of active database rules using symbolic model checking. In 5th East European Conference on Advances in Databases and Information Systems, ADBIS ’01, Vilnius, Lithuania, 25–28 Sept. 2001 (pp. 266–279). London, UK: Springer.
  84. Royer, J. (2001). Formal specification and temporal proof techniques for mixed systems. In Proceedings 15th International Parallel and Distributed Processing Symposium. IPDPS 2001, San Francisco, CA, 23–27 April 2001 (pp. 1542–1551). New York, NY: IEEE Comput. Soc.
  85. Schmid, H. A., & Best, E. (1978). A step towards a solution of the liveness problem in Petri nets. Newcastle upon Tyne. Url:
  86. Sharma, N. K., & Bhargava, B. (1987). A robust distributed termination detection algorithm, Report 87-726. West Lafayette, IN. Url:
  87. Shi, L., & Liu, Y. (2010). Modeling and verification of transmission protocols: A case study on CSMA/CD protocol. In SSIRI-C 2010—4th IEEE International Conference on Secure Software Integration and Reliability Improvement Companion, Singapore, 9-11 June 2010 (pp. 143–149). Washington: IEEE Computer Society.
  88. Singhal, M. (1989). Deadlock detection in distributed systems. Computer, 22(11), 37–48. Scholar
  89. Tricas, F., Colom, J. M., & Merelo, J. J. (2014). Computing minimal siphons in Petri Net models of resource allocation systems: An evolutionary approach. In CEUR Workshop Proceedings CEUR Workshop Proceedings, Petri Nets and Software Engineering, Tunis, Tunisia, 23–24 June 2014 (Vol. 1160, pp. 307–322). Tunis.
  90. Tricas F, Garcia-Valles, F., … Ezpeleta, J. (2005). A Petri net structure—based deadlock prevention solution for sequential resource allocation systems. In 2005 IEEE International Conference on Robotics and Automation, Barcelona, Spain, 18–22 April 2005 (pp. 271–277). New York, NY: IEEE.
  91. Valmari, A. (1994). State of the art report: STUBBORN SETS. Petri Net Newsletter, 46, 6–14. Url: Scholar
  92. Valmari, A., & Hansen, H. (2010). Can stubborn sets be optimal? In 31st International Conference, PETRI NETS 2010, Braga, Portugal, 21–25 June 2010 (pp. 43–62). Heidelberg: Springer.
  93. Węgrzyn, A., Karatkevich, A., & Bieganowski, J. (2004). Detection of deadlocks and traps in petri nets by means of Thelen’s prime implicant method. International Journal of Applied Math and Computer Science, 14(1), 113–121. Url:
  94. Yang, Y., Chen, X., & Gopalakrishnan, G. (2008). Inspect: A runtime model checker for multithreaded C programs, Report UUCS-08-004. Salt Lake City, UT. Url:
  95. Yeung, C.-F., Huang, S.-L., … Law, C.-K. (1994). A new distributed deadlock detection algorithm for distributed database systems. In TENCON’94—1994 IEEE Region 10’s 9th Annual International Conference on: “Frontiers of Computer Technology”, Singapore, 22–26 Aug. 1994 (Vol. 1, pp. 506–510). IEEE.
  96. Zhang, H., Aoki, T., & Chiba, Y. (2015). A spin-based approach for checking OSEK/VDX applications. In C. Artho & P. C. Ölveczky (Eds.), FTSCS 2014: Formal Techniques for Safety-Critical Systems, Luxembourg, 6–7 Nov. 2014 (pp. 239–255). Cham, Switzerland: Springer.
  97. Zhou, J., Chen, X., … Chen, D. (2004). M-Guard: A new distributed deadlock detection algorithm based on mobile agent technology. In 2nd International Conference on Parallel and Distributed Processing and Applications ISPA’04, Hong Kong, China, 13–15 Dec. 2004 (pp. 75–84). Heidelberg: Springer.

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.Institute of Computer ScienceWarsaw University of TechnologyWarsawPoland

Personalised recommendations