MobilityReadingGroup

Protocol-Based Verification of Message-Passing Parallel Programs

Hugo A.LÓPEZ, Eduardo R.B.MARQUES, Francisco MARTINS, Nicholas NG, César SANTOS, Vasco THUDICHUMVASCONCELOS, Nobuko YOSHIDA

We present ParTypes, a type-based methodology for the verification of Message Passing Interface (MPI) programs written in the C programming language. The aim is to statically verify programs against protocol specifications, enforcing properties such as fidelity and absence of deadlocks. We develop a protocol language based on a dependent type system for message-passing parallel programs, which includes various communication operators, such as point-to-point messages, broadcast, reduce, array scatter and gather. 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 C. We successfully verified several MPI programs in a running time that is independent of the number of processes or other input parameters. This contrasts with alternative techniques, notably model checking and runtime verification, that suffer from the state-explosion problem or that otherwise depend on parameters to the program itself. We experimentally evaluated our approach against state-ofthe-art tools for MPI to conclude that our approach offers a scalable solution.

@inproceedings{LMMNSVY2015,
  author = {Hugo A. López and Eduardo R. B. Marques and Francisco Martins and Nicholas Ng and César Santos and Vasco Thudichum Vasconcelos and Nobuko Yoshida},
  title = {{Protocol-Based Verification of Message-Passing Parallel Programs}},
  booktitle = {2015 ACM International Conference on Object Oriented Programming Systems Languages & Applications / SPLASH '15},
  pages = {280--298},
  publisher = {ACM},
  year = 2015
}

@inproceedings{LMMNSVY2015,
  author = {Hugo A. López and Eduardo R. B. Marques and Francisco Martins and Nicholas Ng and César Santos and Vasco Thudichum Vasconcelos and Nobuko Yoshida},
  title = {{Protocol-Based Verification of Message-Passing Parallel Programs}},
  booktitle = {2015 ACM International Conference on Object Oriented Programming Systems Languages & Applications / SPLASH '15},
  pages = {280--298},
  publisher = {ACM},
  doi = "10.1145/2814270.2814302",
  year = 2015
}