Sciweavers

Share
IPPS
2007
IEEE

Formal Analysis for Debugging and Performance Optimization of MPI

12 years 4 months ago
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...
Ganesh Gopalakrishnan, Robert M. Kirby
Added 03 Jun 2010
Updated 03 Jun 2010
Type Conference
Year 2007
Where IPPS
Authors Ganesh Gopalakrishnan, Robert M. Kirby
Comments (0)
books