[FKNS14]
V. Forejt, D. Kroening, G. Narayanaswamy and S. Sharma.
Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs.
In Jones, Cliff and Pihlajasaari, Pekka and Sun, Jun (editors), FM 2014, volume 8442 of Lecture Notes in Computer Science, pages 263-278, Springer.
2014.
[pdf]
[bib]
|
Notes:
The final publication is available at www.springer.com.
The original publication is available at link.springer.com.
|
Abstract.
The Message Passing Interface (MPI) is the standard API
for high-performance and scientific computing. Communication dead-
locks are a frequent problem in MPI programs, and this paper addresses
the problem of discovering such deadlocks. We begin by showing that
if an MPI program is single-path, the problem of discovering communication deadlocks is NP-complete. We then present a novel propositional
encoding scheme which captures the existence of communication dead-
locks. The encoding is based on modelling executions with partial orders,
and implemented in a tool called MOPPER. The tool executes an MPI
program, collects the trace, and builds a SAT formula from the trace
using the propositional encoding scheme. Finally, we present experimental results that quantify the benefit of the approach in comparison to a
dynamic analyser and demonstrate that it offers a scalable solution.
|