DescriptionMPI is a message passing based programming model for distributed-memory parallelism that has been had been widely used for programming supercomputers for over 25 years. However, debugging and verification of MPI programs is widely recognized to be a deep technical challenge. This challenge is further exacerbated by a recent increase in the use of nonblocking MPI operations that bring new classes of bugs related to data races.
In this paper, we introduce a new MPI program debugging approach based on partial symbolic execution so as to avoid the false alarms inherent in the static analysis based methodology. Compared with the dynamic approach, our approach can be applied to incomplete programs and explore multiple execution paths, thereby bringing more flexibility and precision. By comparing with well known static/dynamic tools on real-world MPI applications, our approach shows same precision as the dynamic tool and avoids false positive produced by the static tool.