Detecting deadlock in programs with data-centric synchronization
Daniel Marino, Christian Hammer, Julian Dolby, Mandana Vaziri, Frank Tip, Jan Vítek · 2013
Abstract—Previously, we developed a data-centric approach to concurrency control in which programmers specify synchronization constraints declaratively, by grouping shared locations into atomic sets. We implemented our ideas in a Java extension called AJ, proved that atomicity violations are prevented by construction, and demonstrated that realistic Java programs can be refactored into AJ without significant loss of performance. This paper presents an algorithm for detecting possible deadlock in AJ programs by ordering the locks associated with atomic sets. In our approach, a simple type-based static analysis is extended to handle recursive data structures by considering programmer-supplied lock ordering annotations. In an evaluation of the algorithm on 10 AJ programs, all of these programs were shown to be deadlock-free. Only 4 ordering annotations were needed, in one program and 2 programs required some minor refactorings. For the remaining 7 programs, no programmer intervention of any kind was required. I.