Wed 28 Oct 2015 16:37 - 17:00 at Grand Station 1 - 4. Concurrency Chair(s): Wolfgang De Meuter

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-of-the-art tools for MPI to conclude that our approach offers a scalable solution.

Wed 28 Oct

oopsla2015
15:30 - 17:00: OOPSLA - 4. Concurrency at Grand Station 1
Chair(s): Wolfgang De MeuterVrije Universiteit Brussel
oopsla201515:30 - 15:52
Talk
Peizhao OuUniversity of California at Irvine, USA, Brian DemskyUniversity of California at Irvine, USA
DOI
oopsla201515:52 - 16:15
Talk
Swarnendu BiswasOhio State University, USA, Minjia ZhangOhio State University, USA, Michael BondOhio State University, USA, Brandon LuciaCarnegie Mellon University, USA
DOI Pre-print
oopsla201516:15 - 16:37
Talk
Nachshon CohenTechnion, Israel, Erez PetrankTechnion, Israel
DOI
oopsla201516:37 - 17:00
Talk
Hugo LópezTechnical University of Denmark, Eduardo MarquesUniversity of Lisbon, Portugal, Francisco MartinsUniversity of Lisbon, Portugal, Nicholas NgImperial College London, UK, César SantosUniversity of Lisbon, Portugal, Vasco VasconcelosUniversity of Lisbon, Portugal, Nobuko YoshidaImperial College London, UK
Link to publication