Static-analysis assisted dynamic verification of MPI waitany programs (Poster Abstract)

Abstract

It is well known that the number of schedules (interleavings) of a concurrent program grows exponentially with the number of processes. Our previous work has demonstrated the advantages of an MPI-specific dynamic partial order reduction (DPOR, [5]) algorithm called POE in a tool called ISP [1,2,3] in dramatically reducing the number of interleavings during formal dynamic verification. Higher degrees of interleaving reduction were achieved when the programs were deterministic. In this work, we consider the problem of verifying MPI using MPI-Waitany (and related operations wait/test some/all). Such programs potentially have a higher degree of non-determinism. For such programs, POE can become ineffective, as shown momentarily. To solve this problem, we employ static analysis (supported by ROSE [4]) in a supporting role to POE to determine the extent to which the out parameters of MPI-Waitany can affect subsequent control flow statements. This informs ISP's scheduler to exert even more intelligent backtrack/replay control. © 2009 Springer Berlin Heidelberg.