Paper Info
Title
Practical Formal Verification of MPI and Thread Programs
Abstract
Large-scale simulation codes in science and engineering are written using the Message Passing Interface (MPI). Shared memory threads are widely used directly, or to implement higher level programming abstractions. Traditional debugging methods for MPI or thread programs are incapable of providing useful formal guarantees about coverage. They get bogged down in the sheer number of interleavings (schedules), often missing shallow bugs. In this tutorial we will introduce two practical formal verification tools: ISP (for MPI C programs) and Inspect (for Pthread C programs). Unlike other formal verification tools, ISP and Inspect run directly on user source codes (much like a debugger). They pursue only the relevant set of process interleavings, using our own customized Dynamic Partial Order Reduction algorithms. For a given test harness, DPOR allows these tools to guarantee the absence of deadlocks, instrumented MPI object leaks and communication races (using ISP), and shared memory races (using Inspect). ISP and Inspect have been used to verify large pieces of code: in excess of 10,000 lines of MPI/C for ISP in under 5 seconds, and about 5,000 lines of Pthread/C code in a few hours (and much faster with the use of a cluster or by exploiting special cases such as symmetry) for Inspect. We will also demonstrate the Microsoft Visual Studio and Eclipse Parallel Tools Platform integrations of ISP (these will be available on the LiveCD).
Year
DOI
Venue
2009
10.1007/978-3-642-03770-2_7
PVM/MPI
Keywords
Field
DocType
pthread c program,instrumented mpi object leak,practical formal verification,formal verification tool,thread programs,large-scale simulation code,mpi c program,useful formal guarantee,shared memory thread,c code,practical formal verification tool,process interleavings,formal verification,message passing interface,source code,partial order reduction,shared memory
Programming language,Shared memory,Source code,Debugger,Computer science,Microsoft Visual Studio,POSIX Threads,Message Passing Interface,Operating system,Debugging,Formal verification
Conference
Citations 
PageRank 
References 
1
0.37
1
Authors
2
Name
Order
Citations
PageRank
Ganesh Gopalakrishnan11619130.11
Robert M. Kirby21443115.55