Publication
Protocol-based verification of MPI programs
| dc.contributor.author | Marques, Eduardo R. B. | por |
| dc.contributor.author | Martins, Francisco | por |
| dc.contributor.author | Vasconcelos, Vasco T. | por |
| dc.contributor.author | Santos, César | por |
| dc.contributor.author | Ng, Nicholas | por |
| dc.contributor.author | Yoshida, Nobuko | por |
| dc.date.accessioned | 2014-10-23T15:51:08Z | por |
| dc.date.accessioned | 2014-11-14T16:24:15Z | |
| dc.date.available | 2014-10-23T15:51:08Z | por |
| dc.date.available | 2014-11-14T16:24:15Z | |
| dc.date.issued | 2014-10-23T15:51:08Z | por |
| dc.description.abstract | We present a methodology for the verification of Message Passing Interface (MPI) programs written in C. The aim is to statically verify programs against protocol specifications, enforcing properties such as fidelity and absence of deadlocks. We make use of a protocol language based on a dependent type system for message-passing parallel programs. % For the verification of a program against a given protocol, the protocol is first translated into a representation read by VCC, a software verifier for the~C programming language. % The program is then annotated with specific assertions that, together with a pre-established set of contracts for MPI primitives, guide the verifier to either prove or disprove the program's conformance to the protocol. We successfully verified MPI programs in a running time that is independent of the number of processes or other input parameters. This contrasts with other techniques, notably model checking and symbolic execution, that suffer from the state-explosion problem. We experimentally evaluated our approach against TASS, a state-of-the-art tool for MPI program verification. | por |
| dc.description.version | Under review | por |
| dc.identifier.uri | http://hdl.handle.net/10451/14267 | por |
| dc.identifier.uri | http://repositorio.ul.pt/handle/10455/6901 | por |
| dc.language.iso | eng | por |
| dc.relation.ispartofseries | 2014;05 | por |
| dc.subject | protocol | por |
| dc.subject | parallel programs | por |
| dc.subject | verification | por |
| dc.subject | MPI | por |
| dc.title | Protocol-based verification of MPI programs | por |
| dc.type | report | |
| dspace.entity.type | Publication | |
| rcaap.rights | openAccess | |
| rcaap.type | report | por |
Files
License bundle
1 - 1 of 1