Paper Info
Title
Scheduling considerations for building dynamic verification tools for MPI
Abstract
Dynamic verification methods are the natural choice for formally verifying real world programs when model extraction and maintenance are expensive. Message passing programs written using the MPI library often fall under this category, especially when these programs have to be verified after being ported to new platforms and iteratively optimized. However, implementing dynamic verification tools for MPI requires solving many problems pertaining to the scheduling realities of the MPI runtime. In this paper, we describe the progression of our ideas during the development of our dynamic verification tool for MPI programs, called in-situ partial order (ISP). Each idea developed in this progression relates to our dual goals of ensuring full coverage of all representative interleavings (in the sense of partial order reduction) among MPI processes, and forcing the MPI runtime to affect these interleavings. We briefly examine similar issued faced by other builders of dynamic verification tools. We conclude with observations backing the growing importance of addressing scheduling issues in future dynamic verification tools for various concurrency APIs.
Year
DOI
Venue
2008
10.1145/1390841.1390844
PADTAD
Keywords
Field
DocType
message passing,mpi,partial order,model checking,partial order reduction,distributed programming
Model checking,Programming language,Computer science,Concurrency,Scheduling (computing),Real-time computing,Porting,Model extraction,Partial order reduction,Message passing,Distributed computing
Conference
Citations 
PageRank 
References 
7
0.60
10
Authors
4
Name
Order
Citations
PageRank
Sarvani Vakkalanka117711.14
Michael Delisi2987.10
Ganesh Gopalakrishnan31619130.11
Robert M. Kirby41443115.55