Paper Info
Title
Formal verification of practical MPI programs
Abstract
This paper considers the problem of formal verification of MPI programs operating under a fixed test harness for safety properties without building verification models. In our approach, we directly model-check the MPI/C source code, executing its interleavings with the help of a verification scheduler. Unfortunately, the total feasible number of interleavings is exponential, and impractical to examine even for our modest goals. Our earlier publications formalized and implemented a partial order reduction approach that avoided exploring equivalent interleavings, and presented a verification tool called ISP. This paper presents algorithmic and engineering innovations to ISP, including the use of OpenMP parallelization, that now enables it to handle practical MPI programs, including:(i)~ParMETIS - a widely used hypergraph partitioner, and (ii)~MADRE - a Memory Aware Data Re-distribution Engine, both developed outside our group. Over these benchmarks, ISP has automatically verified up to 14K lines of MPI/C code, producing error traces of deadlocks and assertion violations within seconds.
Year
DOI
Venue
2009
10.1145/1504176.1504214
Proceedings of the 19th ACM SIGPLAN symposium on Principles and practice of parallel programming
Keywords
Field
DocType
partial order reduction,distributed programming,formal verification,model checking,message passing interface,mpi,software engineering,source code
Test harness,Programming language,Model checking,Source code,Computer science,Theoretical computer science,Message Passing Interface,Partial order reduction,Distributed computing,Shared memory,Parallel computing,Distributed memory,Formal verification
Conference
Volume
Issue
ISSN
44
4
0362-1340
Citations 
PageRank 
References 
45
2.14
18
Authors
6
Name
Order
Citations
PageRank
Vo Anh1124491.60
Sarvani Vakkalanka217711.14
Michael Delisi3987.10
Ganesh Gopalakrishnan41619130.11
Robert M. Kirby51443115.55
Rajeev Thakur63773251.09