We examine the problem of verifying MPI programs for the absence of deadlocks and local assertion violations through dynamic (runtime) formal verification in which the processes of a given MPI program are executed under the control of an interleaving scheduler. The development of such an algorithm requires several challenges to be overcome in ensuring full coverage (as opposed to a testing tool that can miss bugs)

• The algorithm must take into consideration MPI`s out-of-order completion semantics (that is, MPI operations need not finish in the issue order), and
• The algorithm must ensure that MPI wildcard receive matches are considered in all possible ways.

Our new algorithm POE, is based on the following novel ideas. First, it rewrites wildcard receives to specific receives, one for each sender that can potentially match with the receive. It then recursively explores each case of the specific receives. The list of potential senders matching a receive is determined through a runtime algorithm (POE), that exploits MPI` operational ordering semantics. Our verification tool ISP that incorporates this algorithm efficiently verifies several programs and finds bugs in many cases where existing dynamic informal verification tools may miss them.

• Details of POE algorithm can be found here.
• MPI operations currently supported by ISP can be found here.
• Download ISP

This document was translated from L^AT_EX by H^EV^EA.