MPI-checker: static analysis for MPI
This paper presents MPI-Checker, a static analysis checker to verify the correct usage of the MPI API in C and C++ code, based on Clang's Static Analyzer. The checker works with path-sensitive as well as with non-path-sensitive analysis which is purely based on information provided by the abstract syntax tree representation of source code. MPI-Checker's path-sensitive checks verify aspects of nonblocking communication, based on the usage of MPI requests, which are tracked by a symbolic representation of their memory region in the course of symbolic execution. Usage of double nonblocking calls without intermediate wait, nonblocking calls without a matching wait and waiting for a request that was never used by a nonblocking call is currently detected by the checker. AST-based checks verify correct type usage in MPI functions. Further, experimental support to verify if point-to-point function calls have a matching partner or lead to a deadlock is provided. In context of LLVM, each check except the checks regarding correct type usage, provides a completely new addition to the architecture. MPI-Checker works MPI implementation independent. No assumptions about implementation details of an MPI library are made in any of the checks. MPI-Checker introduces only negligible overhead on top of the Clang Static Analyzer core and is able to detect critical bugs in real world codebases, which is shown by evaluating analysis results for the open source projects AMG2013, CombBLAS and OpenFFT.