A Sound Reduction of Persistent-Sets for Deadlock Detection in MPI Applications
A Sound Reduction of Persistent-Sets for Deadlock Detection in MPI Applications
复制标题
MPI 应用程序中用于死锁检测的持久集的健全减少
DOI：
10.1007/978-3-642-33296-8_15
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
G. Bronevetsky
中科院分区：
文献类型：
--
作者：
Subodh Sharma;G. Gopalakrishnan;G. Bronevetsky
消息传递接口（MPI）程序的形式化动态分析在开发HPC应用程序的背景下是至关重要的。现有的MPI程序的动态验证工具遭受指数进度爆炸，特别是当多个非确定性接收语句由一个进程发出。在本文中，我们专注于检测MPI程序中的消息孤立死锁。对于这个分析目标，我们描述了一个健全的启发式，有助于避免在大多数实际情况下的时间表爆炸，而不是在实践中错过死锁。我们的方法取决于最初计算的潜在的非确定性的匹配传统的动态分析，但只包括条目被发现相关的拒绝死锁（本质上是一个宏观的观点持久集减少技术）。实验结果令人鼓舞。
Formal dynamic analysis of Message Passing Interface (MPI) programs is crucially important in the context of developing HPC applications. Existing dynamic verification tools for MPI programs suffer from exponential schedule explosion, especially when multiple non-deterministic receive statements are issued by a process. In this paper, we focus on detecting message-orphaning deadlocks within MPI programs. For this analysis target, we describe a sound heuristic that helps avoid schedule explosion in most practical cases while not missing deadlocks in practice. Our method hinges on initially computing the potential non-deterministic matches as conventional dynamic analyzers do, but then including only the entries which are found relevant to cause a refusal deadlock (essentially a macroscopic-view persistent-set reduction technique). Experimental results are encouraging.