MPI-Checker

Verify the correct usage of the MPI API in C and C++ code, with checks based on Clang’s Static Analyzer and Clang-Tidy.

Integrated checks

Path-Sensitive-Checks

• double nonblocking: Double request usage of nonblocking calls without intermediate wait.
• missing wait: Nonblocking call without matching wait.
• unmatched wait: Waiting for a request that was never used by a nonblocking call.

The path-sensitive checks have been merged into Clang's Static Analyzer and are available since LLVM 3.9.

AST-Checks

• type mismatch: Buffer type and specified MPI type do not match.
• incorrect buffer referencing: Buffer is incorrectly referenced when passed to an MPI function.

The AST-based checks have been merged into Clang-Tidy and are available since LLVM 4.0.

Limitations

• No assumption about run time dependent results can be made.
• Heap allocated MPI_Request variables are not taken into account.
• Analysis is limited to the scope of a translation unit.

A general limitation of static analysis to keep in mind is that basically no assumptions about run time dependent results can be made. In consequence, functions like MPI_Waitany cannot be taken into account. Further, the reasoning about heap allocated memory is limited which is why heap allocated requests are not considered. The problem is that the element count held by the memory region must be known, in order to reason about the single requests. Requests that are not heap allocated themselves but a member of a heap allocated struct or class instance can be taken into account, as their array size can be statically determined. Using the Clang Static Analyzer, the analysis is limited to the scope of a translation unit. Analyzing logic across translation units to detect bugs is therefore not possible. This includes that there is limited knowledge about memory regions returned from functions which are defined in a different translation unit than they are used in. Definitions in header files are inlined and therefore considered during analysis in the translation units that include the headers.

Usage

How to apply the checks

Paper

MPI-Checker – Static Analysis for MPI

Slides

The Second Workshop on the LLVM Compiler Infrastructure in HPC

Code

Path-Sensitive-Checks

• clang/lib/StaticAnalyzer/Checkers/MPI-Checker
• clang/test/Analysis/mpichecker.cpp
• clang/test/Analysis/mpicheckernotes.cpp

AST-Checks

• clang-tools-extra/clang-tidy/mpi
• clang-tools-extra/test/clang-tidy/checkers/mpi/buffer-deref.cpp
• clang-tools-extra/test/clang-tidy/checkers/mpi/type-mismatch.cpp