An Automatic Technique for Static Deadlock Prevention
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.
KeywordsConcurrent Programming Formal Argument Data Race Exclusive Access Deadlock Prevention
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.EVE (Eiffel Verification Environment). http://se.inf.ethz.ch/research/eve/
- 5.Meyer, B.: Steps towards a theory and calculus of aliasing. Int. J. Softw. Inform. 5, 77–116 (2011)Google Scholar
- 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). http://se.inf.ethz.ch/people/morandi/publications/prototyping.pdf
- 8.Nienaltowski, P.: Practical framework for contract-based concurrent object-oriented programming. Ph.D. thesis, ETH Zurich (2007). http://se.inf.ethz.ch/old/people/nienaltowski/papers/thesis.pdf
- 9.SCOOP. http://cme.ethz.ch/