Combining symbolic execution and model checking to verify MPI programs
Hengbiao Yu · 2018
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 non-determinism. 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.