Paper Info
Title
Static-Analysis Assisted Dynamic Verification of MPI Waitany Programs (Poster Abstract)
Abstract
It is well known that the number of schedules (interleavings) of a concurrent program grows exponentially with the number of processes. Our previous work has demonstrated the advantages of an MPI-specific dynamic partial order reduction (DPOR, [5]) algorithm called POE in a tool called ISP [1,2,3] in dramatically reducing the number of interleavings during formal dynamic verification. Higher degrees of interleaving reduction were achieved when the programs were deterministic . In this work, we consider the problem of verifying MPI using MPI_Waitany (and related operations wait/test some/all). Such programs potentially have a higher degree of non-determinism. For such programs, POE can become ineffective, as shown momentarily. To solve this problem, we employ static analysis (supported by ROSE [4]) in a supporting role to POE to determine the extent to which the out parameters of MPI_Waitany can affect subsequent control flow statements. This informs ISP's scheduler to exert even more intelligent backtrack/replay control.
Year
DOI
Venue
2009
10.1007/978-3-642-03770-2_43
PVM/MPI
Keywords
Field
DocType
control flow,partial order reduction,static analysis
Computer science,Static analysis,Control flow,Parallel computing,Schedule,Partial order reduction,Interleaving
Conference
Volume
ISSN
Citations 
5759
0302-9743
2
PageRank 
References 
Authors
0.39
3
6
Name
Order
Citations
PageRank
Sarvani Vakkalanka117711.14
Grzegorz Szubzda251.17
Vo Anh3124491.60
Ganesh Gopalakrishnan41619130.11
Robert M. Kirby51443115.55
Rajeev Thakur63773251.09