Implementing Ecient Dynamic Formal Veri Methods for MPI Programs. (In this proceeding - EuroPVM/MPI

Abstract. We examine the problem of verifying MPI programs for the absence of deadlocks and local assertion violations through dynamic (runtime) formal verication in which the processes of a given MPI pro-gram are executed under the control of an interleaving scheduler. The development of such an algorithm requires several challenges to be over-come in ensuring full coverage (as opposed to a testing tool that can miss bugs): (i) The algorithm must take into consideration MPI's out-of-order completion semantics (that is, MPI operations need not nish in the issue order), and (ii) the algorithm must ensure that MPI wildcard receive matches are considered in all possible ways. Our new algorithm is based on the following novel ideas. First, it rewrites wildcard receives to speci c receives, one for each sender that can potentially match with the receive. It then recursively explores each case of the specic receives. The list of potential senders matching a receive is determined through a run-time algorithm that exploits MPI's operational ordering semantics. Our veri cation tool ISP that incorporates this algorithm eciently veries several programs and nds bugs in many cases where existing dynamic informal verication tools may miss them.