Combining Symbolic Execution and Model Checking to Verify MPI Programs

Message Passing Interface (MPI) has become the standard programming paradigm in high performance computing. It is challenging to verify MPI programs because of high parallelism and nondeterminism. This paper presents MPI symbolic verifier (MPI-SV), the first symbolic execution based tool for verifying MPI programs having both blocking and non-blocking operations. MPI-SV exploits symbolic execution to automatically generate path-level models, and performs model checking on the models w.r.t. expected properties. The results of model checking are leveraged to prune redundant paths. We have implemented MPI-SV and the extensive evaluation demonstrates MPI-SV's effectiveness and efficiency.