一句话：提出基于偏序与命题编码的 MPI 通信死锁预测分析方法，并实现 MOPPER 工具，可扩展地检测单路径程序死锁。
MPI 是高性能与科学计算中的标准并行 API，通信死锁是其程序常见问题。本文研究如何发现此类死锁。作者首先证明，若 MPI 程序只有单一路径，发现通信死锁属于 NP 完全问题；随后提出一种新的命题编码，用偏序建模执行并刻画通信死锁的存在性。该编码实现于工具 MOPPER 中：它执行 MPI 程序、收集轨迹、由轨迹构造公式并检查可满足性。实验与其他分析器对比，量化了方法的收益，并表明其对单路径程序具有可扩展性。
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}
}