The Message Passing Interface (MPI) is the standard API for parallelization in high-performance and scientific computing. Communication deadlocks are a frequent problem in MPI programs, and this article 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 that captures the existence of communication deadlocks. The encoding is based on modeling executions with partial orders and implemented in a tool called MOPPER . The tool executes an MPI program, collects the trace, builds a formula from the trace using the propositional encoding scheme, and checks its satisfiability. Finally, we present experimental results that quantify the benefit of the approach in comparison to other analyzers and demonstrate that it offers a scalable solution for single-path programs.

@article{ForejtKNS14,
  title = {Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs},
  author = {Vojtǎch Forejt and Saurabh Joshi and Daniel Kroening and Ganesh Narayanaswamy and Subodh Sharma},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {39},
  number = {4},
  year = {2017},
  doi = {10.1145/3095075}
}