A common problem in MPI programs is deadlock: when two or more processes are blocked indefinitely due to a circular communication dependency. Automatically detecting deadlock is difficult due to its schedule-dependent nature. This paper presents a predictive analysis for single-path MPI programs that observes a single program execution and then determines whether any other feasible schedule of the program can lead to a deadlock. The analysis works by identifying problematic communication patterns in a dependency graph to form a set of deadlock candidates. The deadlock candidates are filtered by an abstract machine and ultimately tested for reachability by an SMT solver with an efficient encoding for deadlock. This approach quickly yields a set of high probability deadlock candidates useful for reasoning about complex codes and yields higher performance overall in many cases compared to other state-of-the-art analyses. The analysis is sound and complete for single-path MPI programs on a given input.
Tue 22 SepDisplayed time zone: (UTC) Coordinated Universal Time change
02:20 - 03:20
|Accelerating All-SAT Computation with Short Blocking Clauses
|A Predictive Analysis for Detecting Deadlock in MPI Programs
Yu Huang Southwestern University of Finance and Economics, Benjamin Ogles Brigham Young University, Eric Mercer Brigham Young UniversityPre-print
|Proving Termination by k-Induction