CSR-SMA: Toward Reliable and Efficient Message Passing Software Through Formal Analysis

University Of Utah, Salt Lake City UT

Investigators

Abstract

The quest for high performance drives parallel scientific computing software design. Well over 60% of the high-performance computing (HPC) community writes programs using the MPI library; to gain performance, they are known to perform many manual optimizations. Even groups that generate MPI from high level descriptions ultimately seem to generate MPI code, due to its eminent portability. However, since performance does not port, manual tweaks are inevitable. This, together with the vastness and evolving nature of the MPI standard, and the innate complexity of concurrent programming introduces costly bugs. Formal methods are enjoying an explosive growth precisely to help eliminate these kinds of bugs. Already they find applications in diverse areas ranging from formally verifying optimizing compiler transformations, formally debugging device driver codes, and solidifying industrial standards. The project will investigate and employ a number of complementary formal approaches to HPC software design: erect formal standards for MPI so that designers are properly educated, take advantage of the standards and write comprehensive MPI platform tests, extract finite-state models from MPI programs and analyze them automatically for deadlocks and race conditions, and will instrument the MPI-based program with correctness assertions that can be checked at run-time. The project will advance the state of the art in formal methods by developing algorithms that take advantage of semantic properties of communication libraries. It will help advance the state of the art in parallel scientific programming by encouraging the use of formal assertions, and encouraging the use of formal analysis in lieu of brute-force execution.