An Integration of Dynamic MPI Formal Verification Within Eclipse PTP
SESSION: Student Poster Reception
EVENT TYPE: Poster, ACM Student Poster
TIME: 5:15PM - 7:00PM
ABSTRACT: The shift from sequential to parallel and distributed computing is of fundamental importance to the advancement of computing practices. Unfortunately such programs are difficult to develop and error-prone. The Message Passing Interface (MPI) is currently the predominant library for parallel programming. Effectively debugging and verifying MPI program correctness proves difficult due to challenges involved with collecting dynamic information about MPI programs and a lack of visual debugging and analysis tools currently available.
Our project develops a powerful array of visual debugging and analysis tools for MPI programs, using a dynamic verification engine called In-situ Partial Order (ISP) that was developed at the University of Utah. ISP is guaranteed to find all deadlocks, assertion violations and MPI object leaks. One major limitation of ISP, when used by itself, is the lack of a powerful and widely usable graphical front-end. Our research has primarily focused on making ISP easier to use and understand by creating a graphical user interface. We now present a new tool called Graphical Explorer of MPI Programs (GEM) that overcomes this limitation and helps users debug and understand MPI programs. GEM effectively offers push-button dynamic formal verification with a rich set of graphical tools to analyze MPI runtime information at several levels of granularity.
For MPI errors, at the push of a button, GEM displays all lines of code involved in any given error detected by ISP. GEM also provides facilities for viewing point-to-point and collective operations of an MPI program. The combination of these features makes ISP a much more viable tool as it has overcome some of the fundamental issues involved with MPI application development.
Our research greatly benefited from mentoring by researchers at IBM Corporation, notably Drs. Beth Tibbitts and Greg Watson. In fact, GEM was contributed to the Eclipse Parallel Tools Platform (PTP), and is available in PTP versions 3.0 & 4.0. This work places ISP prominently in the community of formal verification tools for MPI.
In presenting this poster at SC’10, I will be present at its display to answer any questions regarding our research. I will also have a laptop available for demonstrations of our tool.