MobilityReadingGroup

π-calculus, Session Types research at Imperial College

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
2015 ACM International Conference on Object Oriented Programming Systems Languages & Applications / SPLASH '15 (OOPSLA'15) p. 280 - 298

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}},
  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
}