Semantics Driven Dynamic Partial-order Reduction of MPI-based Parallel Programs (full version

Most distributed parallel programs in the high performance computing (HPC) arena are written using the MPI library. There is growing interest in using model checking for de-bugging these MPI programs. In this context, partial-order reduction has considerable potential for containing state ex-plosion, given the distributed memory nature of MPI pro-grams. This potential is largely unmet. In this paper, we rst dene the formal semantics for a non-trivial subset of MPI. We then prove independence theorems based on the formal semantics, paving the way to a semantically clear and general partial-order reduction approach for MPI. Our work describes, for the rst time, the exact dependencies between MPI non-blocking send operations and their tests for completion, namely wait and test. We also oer a cleaner solution than in previous works for MPI wildcard receives, a proper handling of which requires knowledge of the future course of computations. We show that Flanagan and Gode-froid's dynamic partial-order reduction algorithm oers a natural way to handle the need for future information. Our initial experimental results are encouraging