Contracts for message-passing programs

Abstract

Message-passing parallelism is widely used in High Performance Computing (HPC), and will continue to be used in the foreseeable future. HPC applications perform complex and expensive computations that are of fundamental importance for science, engineering, and society. It is therefore critical that these programs are correct, and effective methods for verifying the correctness of message-passing programs are needed. ☐ This dissertation presents a new method for specifying and verifying correctness of message-passing programs. The method is based on procedure contracts. These provide a natural and intuitive way to decompose the specification and verification tasks. ☐ While procedure contracts have been widely-studied for sequential programs, it is not obvious how to generalize them for message-passing parallel programs. The approach presented here is based on the notion of collective contract, which is analogous to the notion of collective function in message-passing programming. ☐ The first contribution of this dissertation is a rigorous theory of collective con- tracts, presented using a “toy” message-passing language. Second, we present an automated approach for verifying such contracts, given a bound on the number of processes, using model checking and symbolic execution techniques. Our third contribution is a specification language for C/MPI programs, which deals with many of the complexities of those languages. Finally, we have implemented a verifier for specified C/MPI programs using a general verification framework, CIVL. This system is evaluated with a number of simple, but realistic, C/MPI programs.