MobilityReadingGroup

Towards deductive verification of MPI programs against session types

Eduardo R.B.MARQUES, Francisco MARTINS, Vasco THUDICHUMVASCONCELOS, Nicholas NG, Nuno DIASMARTINS

The Message Passing Interface (MPI) is the de facto standard message-passing infrastructure for developing parallel applications. Two decades after the first version of the library specification, MPI-based applications are nowadays routinely deployed on super and cluster computers. These applications, written in C or Fortran, exhibit intricate message passing behaviours, making it hard to statically verify important properties such as the absence of deadlocks. Our work builds on session types, a theory for describing protocols that provides for correct-by-construction guarantees in this regard. We annotate MPI primitives and C code with session type contracts, written in the language of a software verifier for C. Annotated code is then checked for correctness with the software verifier. We present preliminary results and discuss the challenges that lie ahead for verifying realistic MPI program compliance against session types.

@inproceedings{MMVNM2013,
  author = {Eduardo R. B. Marques and Francisco Martins and Vasco Thudichum Vasconcelos and Nicholas Ng and Nuno Dias Martins},
  title = {{Towards deductive verification of MPI programs against session types}},
  booktitle = {5th International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software},
  series = {EPTCS},
  volume = {137},
  pages = {103--113},
  publisher = {Open Publishing Association},
  year = 2013
}

@inproceedings{MMVNM2013,
  author = {Eduardo R. B. Marques and Francisco Martins and Vasco Thudichum Vasconcelos and Nicholas Ng and Nuno Dias Martins},
  title = {{Towards deductive verification of MPI programs against session types}},
  booktitle = {5th International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software},
  series = {EPTCS},
  volume = {137},
  pages = {103--113},
  publisher = {Open Publishing Association},
  doi = "10.4204/EPTCS.137.9",
  year = 2013
}