This article presents a static deadlock analysis for single-path MPI programs. Deadlock is when processes are blocked indefinitely by a circular communication dependency. A single path program is one that does not decode messages for control flow. The analysis records a program execution in the form of a trace and then determines from that trace whether there exists any feasible deadlocking schedules. The primary contribution is the combining of identical consecutive sends or receives into single macro actions. This simplified trace is analyzed for potential deadlock cycles. An abstract machine identifies infeasible cycles, and those not identified by the machine are encoded as satisfiability problems for an SMT solver to resolve. The action combination reduces the complexity of identifying and filtering cycles before needing the costly SMT solver. This article shows the effectiveness of the action combination in experiments on a benchmark suite comparing to traces without action combination and other state-of-the-art deadlock analyses.

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.

Task parallel programming models such as Habanero Java help developers write idiomatic parallel programs and avoid common errors. Data race freedom is a desirable property for task parallel programs but is difficult to prove because every possible execution of the program must be considered. A partial order over events of an observed program execution induces an equivalence class of executions that the program may also produce. The Does-not-Commute (DC) relation is an efficiently computable partial order used for data race detection. As a relatively weak partial order, the DC relation can represent relatively large equivalence classes of program executions. However, some of these executions may be infeasible, thus leading to false data race reports. The contribution of this paper is a mechanized proof that the DC relation is actually sound for commonly used task parallel programming models. Sound means that the first data race identified by the DC relation is guaranteed to be a real data race. A prototype analysis in the Java Pathfinder model checker shows that the DC relation can significantly reduce the number of explored states required to prove data race freedom in Habanero Java programs. In this application, the search for data race using the DC relation is both sound and complete.