Automatic Formal Verification of MPI-Based Parallel Programs

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://vsl.cis.udel.edu/tass under the Gnu Public License.

@inproceedings{siegel-zirkel:2011:ppopp,
	Author = {Stephen F. Siegel and Timothy K. Zirkel},
	Crossref = {ppopp2011},
	Title = {Automatic Formal Verification of {MPI}-Based Parallel Programs},
	Pages = {309--310}
}
@proceedings{ppopp2011,
	Title = {Proceedings of the 16th ACM SIGPLAN Annual Symposium on Principles and Practices of Parallel Programming (PPoPP '11)},
	Booktitle = {Proceedings of the 16th ACM SIGPLAN Annual Symposium on Principles and Practices of Parallel Programming (PPoPP '11)},
	Publisher = {ACM},
	Editor = {Calin Cascaval and Pen-Chung Yew},
	Year = {2011}
}