Clone wiki

armus / PPoPP15

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.

Download the extended version of our PPoPP paper.

Our tool and benchmark data have been evaluated by the Artifact Evaluation Committee of PPoPP '15

Virtual machine appliance

We provide a virtual machine appliance with the source code, compiled binaries, and usage instructions:

Download virtual appliance (direct link, mirror file Armus.ova (sha1sum 84e238969e67babc24538553c822eb200a0adea6, size 1.7G). Usage:

  1. Start VirtualBox.
  2. Import the appliance file Armus.ova (File > Import Appliance ...).
  3. Boot the Armus machine (a browser and a terminal will be available).
  4. Follow the instructions in the browser.

If necessary, the appliance's username is armus and password armus.

Building the source code

Minimum requirements:

To build JArmus:

git clone -b 2.0
cd jarmus
The usage instructions are available in JArmus' project page. The source code is alternatively available in an archive format.

To build Armus-X10:

git clone -b 2.0
cd armus-x10

The usage instructions are available in Armus-X10' project page. The source code is alternatively available in an archive format.

Continue to the description of PPoPP15-Benchmarks

Versions used in this paper: Armus 2.0, JArmus 2.0, and Armus-X10 2.0.