MobilityReadingGroup

Verification of MPI Programs Using Session Types

Kohei HONDA, Eduardo R.B.MARQUES, Francisco MARTINS, Nicholas NG, Vasco THUDICHUMVASCONCELOS, Nobuko YOSHIDA

Developing safe, concurrent (and parallel) software systems is a hard task in multiple aspects, particularly the sharing of information and the synchronization among multiple participants of the system. In the message passing paradigm, this is achieved by sending and receiving messages among different participants, raising a number of verification problems. For instance, exchanging messages in a wrong order may prevent the system from progressing, causing a deadlock.MPI is the most commonly used protocol for high-performance, message-based parallel programs, and the need for formal verification approaches is well acknowledged by much recent work (e.g., see [1]).

@inproceedings{HMMNVY2012,
  author = {Kohei Honda and Eduardo R. B. Marques and Francisco Martins and Nicholas Ng and Vasco Thudichum Vasconcelos and Nobuko Yoshida},
  title = {{Verification of MPI Programs Using Session Types}},
  booktitle = {19th European MPI Users' Group Meeting},
  series = {LNCS},
  volume = {7490},
  pages = {291--293},
  publisher = {Springer},
  year = 2012
}

@inproceedings{HMMNVY2012,
  author = {Kohei Honda and Eduardo R. B. Marques and Francisco Martins and Nicholas Ng and Vasco Thudichum Vasconcelos and Nobuko Yoshida},
  title = {{Verification of MPI Programs Using Session Types}},
  booktitle = {19th European MPI Users' Group Meeting},
  series = {LNCS},
  volume = {7490},
  pages = {291--293},
  publisher = {Springer},
  doi = "10.1007/978-3-642-33518-1_37",
  year = 2012
}