MPI 同步通信程序基本模型中的死锁检测

本文提出了 MPI 同步通信程序的模型，并定义了其三种基本简化模型。给出并严格证明了用于判定这三种模型是否会发生死锁的一系列定理和方法。这些针对简单模型死锁检测的理论与方法是实际 MPI 程序死锁检测的必要基础。这些方法基于对程序的静态分析，并在必要时结合运行时检测，能够针对三种基本模型中的两种在编译前判定是否会发生死锁。对于另一种模型，部分死锁情况可在编译前发现，其余则在运行时发现。我们的定理可用于证明当前流行的 MPI 程序死锁检测算法的正确性。我们的方法可减少那些算法需要修改的 MPI 源代码或性能分析接口的代码量，并能在程序执行前检测死锁，从而大幅降低开销。