Static Deadlock Detection in MPI Synchronization Communication

TL;DR

This paper presents a static analysis approach for detecting deadlocks in MPI synchronization communication, introducing models of varying complexity and a Java-based framework that outperforms dynamic methods in deadlock detection.

Contribution

It develops a static deadlock detection method for MPI programs using models of different complexities and implements a Java framework that detects deadlocks before runtime.

Findings

The framework effectively detects deadlocks in MPI programs.

Static analysis can outperform dynamic methods in deadlock detection.

The models cover sequential, single-loop, and nested-loop MPI communication patterns.

Abstract

It is very common to use dynamic methods to detect deadlocks in MPI programs for the reason that static methods have some restrictions. To guarantee high reliability of some important MPI-based application software, a model of MPI synchronization communication is abstracted and a type of static method is devised to examine deadlocks in such modes. The model has three forms with different complexity: sequential model, single-loop model and nested-loop model. Sequential model is a base for all models. Single-loop model must be treated with a special type of equation group and nested-loop model extends the methods for the other two models. A standard Java-based software framework originated from these methods is constructed for determining whether MPI programs are free from synchronization communication deadlocks. Our practice shows the software framework is better than those tools using dynamic methods because it can dig out all synchronization communication deadlocks before an MPI-based program goes into running.