Dynamic deadlock verification for general barrier synchronisation
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.
The Armus-X10 and JArmus applications are the first deadlock
verification tools for X10 clocks and the Java phaser API, featuring:
distributed deadlock detection where the tool reports existing
deadlocks, and local deadlock avoidance where the tool
raises an exception before entering a deadlock.
Virtual machine appliance
We provide a virtual machine appliance with the source code, compiled binaries, and usage instructions:
- Start VirtualBox.
- Import the appliance file
Import Appliance ...).
- Boot the Armus machine (a browser and a terminal will be available).
- Follow the instructions in the browser.
If necessary, the appliance's username is
armus and password
Building the source code
To build JArmus:
git clone https://bitbucket.org/cogumbreiro/jarmus -b 2.0 cd jarmus ant
To build Armus-X10:
git clone https://bitbucket.org/cogumbreiro/armus-x10 -b 2.0 cd armus-x10 ant
Continue to the description of PPoPP15-Benchmarks