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