Name
Abstract | ||
|---|---|---|
There is growing need to develop formal verification tools for Message Passing Interface (MPI) programs to eliminate bugs such as deadlocks and local assertion violations. Of all approaches, dynamic verification is most practical for MPI. Since the number of interleavings of concurrent programs grow exponentially, we devise a dynamic interleaving reduction algorithm (dynamic partial order reduction , DPOR) tailor-made for MPI, called POE. The key contributions of this paper are: (i) a formal semantics that elucidates the complex dynamic semantics of MPI, and played an essential role in the design of the POE algorithm and the construction of the ISP tool, and (ii) a formal specification of our POE algorithm. We discuss how these ideas may help us build dynamic verifiers for other APIs, and summarize a dynamic verifier being designed for applications written using a recently proposed API for multi-core communication. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/978-3-642-05089-3_46 | FM |
Keywords | Field | DocType |
partial order reduction,complex dynamics,formal verification,formal specification,formal semantics | Programming language,Computer science,Program counter,Deadlock,Theoretical computer science,Formal specification,Message Passing Interface,Formal methods,Partial order reduction,Semantics,Formal verification | Conference |
Volume | ISSN | Citations |
5850 | 0302-9743 | 9 |
PageRank | References | Authors |
0.64 | 18 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sarvani Vakkalanka | 1 | 177 | 11.14 |
| Vo Anh | 2 | 1244 | 91.60 |
| Ganesh Gopalakrishnan | 3 | 1619 | 130.11 |
| Robert M. Kirby | 4 | 1443 | 115.55 |