Dynamic deadlock verification for general barrier synchronisation

Tiago Cogumbreiro, Raymond Hu, Francisco Martins, Nobuko Yoshida

    Research output: Contribution to conferencePaperpeer-review

    13 Citations (Scopus)


    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.
    Original languageEnglish
    Number of pages10
    Publication statusPublished - 24 Jan 2015
    Event20th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming - San Francisco, United States
    Duration: 7 Feb 201511 Feb 2015


    Conference20th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming
    Country/TerritoryUnited States
    CitySan Francisco


    Dive into the research topics of 'Dynamic deadlock verification for general barrier synchronisation'. Together they form a unique fingerprint.

    Cite this