Name
Abstract | ||
|---|---|---|
Formal dynamic analysis of Message Passing Interface (MPI) programs is crucially important in the context of developing HPC applications. Existing dynamic verification tools for MPI programs suffer from exponential schedule explosion, especially when multiple non-deterministic receive statements are issued by a process. In this paper, we focus on detecting message-orphaning deadlocks within MPI programs. For this analysis target, we describe a sound heuristic that helps avoid schedule explosion in most practical cases while not missing deadlocks in practice. Our method hinges on initially computing the potential non-deterministic matches as conventional dynamic analyzers do, but then including only the entries which are found relevant to cause a refusal deadlock (essentially a macroscopic-view persistent-set reduction technique). Experimental results are encouraging. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1007/978-3-642-33296-8_15 | SBMF |
Keywords | Field | DocType |
formal dynamic analysis,sound reduction,analysis target,exponential schedule explosion,dynamic verification tool,multiple non-deterministic,mpi program,mpi application,hpc application,deadlock detection,schedule explosion,conventional dynamic analyzer,potential non-deterministic | Heuristic,Computer science,Deadlock,Program counter,Real-time computing,Message Passing Interface,Deadlock prevention algorithms,Distributed computing | Conference |
Citations | PageRank | References |
2 | 0.37 | 8 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Subodh Sharma | 1 | 70 | 5.99 |
| Ganesh Gopalakrishnan | 2 | 1619 | 130.11 |
| Greg Bronevetsky | 3 | 949 | 44.91 |