Precise predictive analysis for discovering communication deadlocks in MPI programs

Vojt?ch Forejt Saurabh Joshi Daniel Kroening Ganesh Narayanaswamy Subodh Sharma
Abstract 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 ...