MobilityReadingGroup

Deductive Verification of MPI Protocols

Vasco T.VASCONCELOS, Francisco MARTINS, Eduardo R.B.MARQUES, Nobuko YOSHIDA, Nicholas NG

This chapter presents the PARTYPES framework to statically verify C programs that use the Message Passing Interface, the widely used standard for message-based parallel applications. Programs are checked against a protocol specification that captures the interaction in an MPI program. The protocol language is based on a dependent type system that is able to express various MPI communication primitives, including point-to-point and collective operations. The verification uses VCC, a mechanical verifier for concurrent C programs. It takes the program protocol written in VCC format, an annotated version of the MPI library, and the program to verify, and checks whether the program complies with the protocol.

@article{VMMYN2017,
  author = {Vasco T. Vasconcelos and Francisco Martins and Eduardo R.B. Marques and Nobuko Yoshida and Nicholas Ng},
  title = {{Deductive Verification of MPI Protocols}},
  journal = {Behavioural Types: from Theory to Tools},
  pages = {353--372},
  publisher = {River Publishers},
  year = 2017
}

@article{VMMYN2017,
  author = {Vasco T. Vasconcelos and Francisco Martins and Eduardo R.B. Marques and Nobuko Yoshida and Nicholas Ng},
  title = {{Deductive Verification of MPI Protocols}},
  journal = {Behavioural Types: from Theory to Tools},
  pages = {353--372},
  publisher = {River Publishers},
  doi = "10.13052/rp-9788793519817",
  year = 2017
}