An Automatic Technique for Static Deadlock Prevention

  • Bertrand MeyerEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8974)


Deadlocks remain one of the biggest threats to concurrent programming. Usually, the best programmers can expect is dynamic deadlock detection, which is only a palliative. Object-oriented programs, with their rich reference structure and the resulting presence of aliasing, raise additional problems. The technique developed in this paper relies on the “alias calculus” to offer a completely static and completely automatic analysis of concurrent object-oriented programs. The discussion illustrates the technique by applying it to two versions of the “dining philosophers” program, of which it proves that the first is deadlock-free and the second deadlock-prone.


Concurrent Programming Formal Argument Data Race Exclusive Access Deadlock Prevention 
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.



The research reported here is part of the Concurrency Made Easy project at ETH, an Advanced Investigator Grant of the European Research Council (ERC grant agreement no. 29138). I am grateful to members of the CME project, particularly Scott West, Benjamin Morandi and Sebastian Nanz, for numerous comments on the research. Alexander Kogtenkov and Sergey Vedler were instrumental in the development of the alias calculus. Victorien Elvinger spotted an error in an earlier version.


  1. 1.
    EVE (Eiffel Verification Environment).
  2. 2.
    Kogtenkov, A., Meyer, B., Velder, S.: Alias calculus, frame calculus and frame inference. Sci. Comput. Program. Part 1 97(1), 163–172 (2015)CrossRefGoogle Scholar
  3. 3.
    Meyer, B.: Systematic concurrent object-oriented programming. Commun. ACM 36(9), 56–80 (1993)CrossRefGoogle Scholar
  4. 4.
    Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice Hall, Upper Saddle River (1997). Chapter 32 includes a description of SCOOPzbMATHGoogle Scholar
  5. 5.
    Meyer, B.: Steps towards a theory and calculus of aliasing. Int. J. Softw. Inform. 5, 77–116 (2011)Google Scholar
  6. 6.
    Meyer, B., Kogtenkov, A.: Negative variables and the essence of object-oriented programming. In: Iida, S., Meseguer, J., Ogata, K. (eds.) Specification, Algebra, and Software. LNCS, vol. 8373, pp. 171–187. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  7. 7.
    Morandi, B., Schill, M., Nanz, S., Meyer, B.: Prototyping a concurrency model. In: International Conference on Application of Concurrency to System Design, pp. 177–186 (2013).
  8. 8.
    Nienaltowski, P.: Practical framework for contract-based concurrent object-oriented programming. Ph.D. thesis, ETH Zurich (2007).
  9. 9.

Copyright information

© Springer-Verlag Berlin Heidelberg 2015

Authors and Affiliations

  1. 1.ETH ZurichZurichSwitzerland
  2. 2.Innopolis UniversityKazanRussia
  3. 3.Eiffel SoftwareGoletaUSA

Personalised recommendations