一句话：提出单路径 MPI 程序的预测分析，通过依赖图、抽象机与 SMT 求解检测其他可行调度下的死锁。
MPI 程序中的死锁由循环通信依赖导致，因调度相关而难以自动检测。本文提出一种针对单路径 MPI 程序的预测分析：仅观察一次程序执行，在通信依赖图中识别有问题的通信模式以形成死锁候选，再用抽象机过滤候选，最终由带高效死锁编码的 SMT 求解器测试可达性。该方法能快速产生高概率死锁候选，有助于理解复杂代码，并在许多情况下性能优于其他先进分析。在给定输入下，该分析对单路径 MPI 程序是可靠且完备的。
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.
DOI 原文 ·
@inproceedings{paperbot5887,
title = {A predictive analysis for detecting deadlock in MPI programs},
author = {Yu Huang and Benjamin Ogles and Eric Mercer},
booktitle = {ASE},
year = {2020},
doi = {10.1145/3324884.3416588}
}