MobilityReadingGroup

Dynamic deadlock verification for general barrier synchronisation

Tiago COGUMBREIRO, Raymond HU, Francisco MARTINS, Nobuko YOSHIDA

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."

@inproceedings{CHMY2015,
  author = {Tiago Cogumbreiro and Raymond Hu and Francisco Martins and Nobuko Yoshida},
  title = {{Dynamic deadlock verification for general barrier synchronisation}},
  booktitle = {20th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming},
  pages = {150--160},
  publisher = {ACM},
  year = 2015
}

@inproceedings{CHMY2015,
  author = {Tiago Cogumbreiro and Raymond Hu and Francisco Martins and Nobuko Yoshida},
  title = {{Dynamic deadlock verification for general barrier synchronisation}},
  booktitle = {20th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming},
  pages = {150--160},
  publisher = {ACM},
  doi = "10.1145/2688500.2688519",
  year = 2015
}