Dynamic deadlock verification for general barrier synchronisation
File(s)
Author(s)
Soares Cogumbreiro Garcia, T
Hu, R
Martins, F
Yoshida, N
Type
Conference Paper
Abstract
We present Armus, a dynamic verification tool for deadlock detection and avoidance specialised in barrier synchronisation. Barriers are used to coordinate the execution of groups of tasks, and serve as a building block of parallel computing. Our tool verifies more barrier synchronisation patterns than current state-of-the-art. To improve the scalability of verification, we introduce a novel event-based representation of concurrency constraints, and a graph-based technique for deadlock analysis. The implementation is distributed and fault-tolerant, and can verify X10 and Java programs. To formalise the notion of barrier deadlock, we introduce a core language expressive enough to represent the three most widespread barrier synchronisation patterns: group, split-phase, and dynamic membership. We propose a graph analysis technique that selects from two alternative graph representations: the Wait-For Graph, that favours programs with more tasks than barriers; and the State Graph, optimised for programs with more barriers than tasks. We prove that finding a deadlock in either representation is equivalent, and that the verification algorithm is sound and complete with respect to the notion of deadlock in our core language. Armus is evaluated with three benchmark suites in local and distributed scenarios. The benchmarks show that graph analysis with automatic graph-representation selection can record a 7-fold execution increase versus the traditional fixed graph representation. The performance measurements for distributed deadlock detection between 64 processes show negligible overheads.
Date Issued
2014-11-10
Date Acceptance
2014-11-10
Citation
Proceedings of the 20th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2014
Journal / Book Title
Proceedings of the 20th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming
Copyright Statement
© ACM, 2015. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Proceedings of the 20th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, http://doi.org/10.1145/2688500.2688519
Source
20th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP 2015)
Publication Status
Accepted
Start Date
2015-02-07
Finish Date
2015-02-11
Coverage Spatial
San Francisco, CA