An efficient technique for deadlock analysis of large scale process networks

  • J. M. R. Martin
  • S. A. Jassim
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1313)


Nowadays we are becoming increasingly dependent on parallel or distributed computer systems for many safety critical applications. Therefore, in order to avoid software precipitated catastrophes, we must look for ways to enable software engineers to design systems that are free from pathological problems such as deadlock. Traditionally deadlock has been one of the most feared problems in parallel computing. Existing tools which perform deadlock analysis can usually cope only with rather small networks due to the problem of exponential state explosion. Here we describe the implementation of a new, highly efficient, graph-theoretical approach to automatically proving deadlock-freedom which can be used to analyse CSP networks of arbitrary size. Our methods exploit previous work by S. D. Brookes, A. W. Roscoe and N. Dathi.


Transition System Process Pair Network Torus Safety Critical Application Dine Philosopher 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    P. Brinch Hansen: Operating System Principles, Prentice-Hall 1973.Google Scholar
  2. 2.
    S. D. Brookes and A. W. Roscoe: Deadlock Analysis in Networks of Communicating Processes, Distributed Computing (1991)4, Springer Verlag.Google Scholar
  3. 3.
    K. M. Chandy and J. Misra: Deadlock Absence Proofs for Networks of Communicating Processes, Information Processing Letters. Volume 9 number 4 1979.Google Scholar
  4. 4.
    N. Dathi: Deadlock and Deadlock-Freedom, Oxford University D. Phil Thesis 1990.Google Scholar
  5. 5.
    E. W. Dijkstra: Cooperating Sequential Processes, Technological University Eindhoven, The Netherlands 1965. (Reprinted in Programming Languages, F. Genuys, ed., Academic Press, New York 1968.)Google Scholar
  6. 6.
    E. W. Dijkstra: A Class of Simple Communication Patterns, Selected Writings on Computing: A Personal Perspective, Springer-Verlag 1982.Google Scholar
  7. 7.
    S. Even: Graph Algorithms, Computer Science Press, Inc. 1979.Google Scholar
  8. 8.
    FDR User Manual and Tutorial: Formal Systems (Europe) Ltd. 3 Alfred Street, Oxford OXl 4EH. Available at Scholar
  9. 9.
    C. A. R. Hoare: Communicating Sequential Processes, Prentice Hall 1985Google Scholar
  10. 10.
    E. Knapp: Deadlock Detection in Distributed Databases, ACM Computing Surveys, Vol 19, No 4, December 1987.Google Scholar
  11. 11.
    J. M. R. Martin: The Design and Construction of Deadlock-Free Concurrent Systems, D. Phil. Thesis, University of Buckingham (Department of Mathematics, Statistics and Computer Science) 1996. Available at Scholar
  12. 12.
    J. M. R. Martin, I. East, and S. Jassim: Design Rules for Deadlock-Freedom, Transputer Communications, September 1994Google Scholar
  13. 13.
    J. M. R. Martin and S. A. Jassim: A Tool for Proving Deadlock Freedom, in Parallel Programming and Java, Proceedings of the 20th World Occam and Transputer User Group Technical Meeting, IOS Press 1997Google Scholar
  14. 14.
    J. M. R. Martin and S. A. Jassim: How to Design Deadlock-Free Networks Using CSP and Verification Tools — A Tutorial Introduction, in Parallel Programming and Java, Proceedings of the 20th World Occam and Transputer User Group Technical Meeting, IOS Press 1997Google Scholar
  15. 15.
    A. N. Parashkevov and J. Yantchev: ARC-A Tool for Efficient Refinement and Equivalence Checking for CSP, IEEE International Conference on Algorithms and Architectures for Parallel Programming (ICA3PP) '96, Singapore 1996.Google Scholar
  16. 16.
    A. W. Roscoe: Routing Messages Through Networks: An Exercise in Deadlock Avoidance, Proceedings of the 7th occam User Group Technical Meeting, IOS Press 1988.Google Scholar
  17. 17.
    A. W. Roscoe: Notes on CSP, Oxford University Lecture Notes 1995Google Scholar
  18. 18.
    A. W. Roscoe and Naiem Dathi: The Pursuit of Deadlock-Freedom, Oxford University Computing Laboratory (Technical Monograph PRG-57) 1986.Google Scholar
  19. 19.
    A. W. Roscoe: Model Checking CSP, A Classical Mind, Prentice Hall 1994.Google Scholar
  20. 20.
    A. W. Roscoe, P. H. B. Gardiner, M. H. Goldsmith, J. R. Hulance, D. M. Jackson and J. B. Scattergood: Hierarchical compression for model-checking CSP or how to check 1020 dining philosophers for deadlock, in TACAS'95 Workshop, pages 133–152, LNCS 1019, Springer-Verlag 1995.Google Scholar
  21. 21.
    P. H. Welch, G. R. R. Justo, and C. J. Willcock: High Level Paradigms for Deadlock-Free High-Performance Systems, Transputer Applications and Systems '93, IOS Press 1993.Google Scholar
  22. 22.
    J. Yantchev and C. R. Jesshope: Adaptive, low latency, deadlock-free packet routing for networks of processors, IEE Proceeding, Vol 136, Pt. E, No 3, May 1989Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • J. M. R. Martin
    • 1
  • S. A. Jassim
    • 2
  1. 1.Oxford University Computing ServicesOxfordUK
  2. 2.Department of Mathematics Statistics, and Computer ScienceUniversity of BuckinghamUK

Personalised recommendations