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

Deadlock Detection in Basic Models of MPI Synchronization Communication Programs

作　　者：廖名学[1] 范植华[1] 

机构地区：[1]中国科学院软件研究所,北京100080

出　　处：《电子学报》2008年第2期402-407,共6页Acta Electronica Sinica

摘　　要：本文提出了MPI程序的同步通信模型及三个基本简化模型,给出了判定这些基本模型是否死锁的方法和定理并予以了严格证明.简化模型的死锁检测理论和方法是真实MPI程序死锁检测的必要基础.这些方法基于程序静态分析,必要时进行运行时检测,它们对两种简化模型可以在程序编译前确定是否死锁,对另外一种模型,在编译前可静态确定部分死锁,运行中可确定其他死锁.我们的理论可以证明MPI程序死锁检测主流算法的正确性,其方法可以减少它们对客户源代码或MPI profiling接口的修改量,从而大大降低死锁检测开销,并可在运行前判定死锁.A model of MPI synchronization communication programs is presented and its three basic simplified models are also defined. A series of theorems and methods for deciding whether deadlocks will occur among the three models are given and proved strictly. These theories and methods for simple models＇ dcadlock detection are the necessary base for real MPI program dcadlock detection. The methods are based on a static analysis through programs and with runtime detection in necessary cases and they are able to determine before compiling whether it will be deadlocked for two of the three basic models. For another model, some deadlock cases can be found before compiling and others at runtime. Our theorems can be used to prove the correctness of currently popular MPI program deadlock detection algorithms. Our methods may decrease codes that those algorithms need to change to MPI source or profiling interface and may detects deadlocks ahead of program execution, thus the overheads can be reduced greatly.

关 键 词：MPI(Message PASSING Interface) 死锁 同步通信 

分 类 号：TP311.1[自动化与计算机技术—计算机软件与理论]