Automatic Formal Verification of MPI-Based Parallel Programs

作者：Siegel Stephen F^*; Zirkel Timothy K

来源：ACM Sigplan Notices, 2011, 46(8): 309-310.

DOI：10.1145/2038037.1941603

• Verification
• Symbolic execution
• MPI
• message-passing
• debugging
• verification

The Toolkit for Accurate Scientific Software (TASS) is a suite of tools for the formal verification of MPI-based parallel programs used in computational science. TASS can verify various safety properties as well as compare two programs for functional equivalence. The TASS front end takes an integer n >= 1 and a C/MPI program, and constructs an abstract model of the program with n processes. Procedures, structs, (multi-dimensional) arrays, heap-allocated data, pointers, and pointer arithmetic are all representable in a TASS model. The model is then explored using symbolic execution and explicit state space enumeration. A number of techniques are used to reduce the time and memory consumed. A variety of realistic MPI programs have been verified with TASS, including Jacobi iteration and manager-worker type programs, and some subtle defects have been discovered. TASS is written in Java and is available from http://vs1.cis.ude1.edu/tass under the Gnu Public License.

• 出版日期2011-8