Towards deductive verification of MPI programs against session types

Eduardo R. B. Marques
(LASIGE/FCUL, Universidade of Lisbon)
Francisco Martins
(LASIGE/FCUL, Universidade of Lisbon)
Vasco T. Vasconcelos
(LASIGE/FCUL, Universidade of Lisbon)
Nicholas Ng
(Imperial College London)
Nuno Martins
(LASIGE/FCUL, Universidade of Lisbon)

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.

In Nobuko Yoshida and Wim Vanderbauwhede: Proceedings 5th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES 2013), Rome, Italy, 23rd March 2013, Electronic Proceedings in Theoretical Computer Science 137, pp. 103–113.
Published: 8th December 2013.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: