Formal Analysis for Debugging and Performance Optimization of MPI

High-end computing is universally recognized to be a strategic tool for leadership in science and technology. A significant portion of high-end computing is conducted on clusters running the Message Passing Interface (MPI) library. MPI has become a de facto standard in HPC. MPI programs, as well as MPI library implementations can be buggy, especially when aiming high performance, and running on or porting onto new platforms. Our recent work has addressed the following areas: A TLA+ Formal Semantics of a large subset of MPI-1; A Microsoft Phoenix based Model Extraction and Analysis Framework for MPI programs; Integration into the Visual Studio Environment for error-trace visualization; A new dynamic partial order reduction algorithm (DPOR) tailored to MPI so that the number of interleavings examined during MPI program verification are dramatically reduced; A program called ‘inspector’ for Analyzing C++ Programs that has found bugs in publicly distributed threaded programs (Inspec...

• Type: Conference
• Year: 2007
• Where: IPPS
• Authors: Ganesh Gopalakrishnan, Robert M. Kirby
• Keywords: Distributed And Parallel Computing, IPPS 2007, MPI Library Implementations, Mpi One-sided Communication, MPI Programs