Abstract
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.
Original language | English |
---|---|
Title of host publication | Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications - OOPSLA 2015 |
Publisher | Association for Computing Machinery |
Publication date | 2015 |
Pages | 280-298 |
ISBN (Print) | 978-1-4503-3689-5 |
DOIs | |
Publication status | Published - 2015 |
Event | OOPSLA'15 - The ACM SIGPLAN conference on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH) - Pittsburgh, United States Duration: 25 Oct 2015 → 30 Oct 2015 http://2015.splashcon.org/ |
Conference
Conference | OOPSLA'15 - The ACM SIGPLAN conference on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH) |
---|---|
Country/Territory | United States |
City | Pittsburgh |
Period | 25/10/2015 → 30/10/2015 |
Other | 2015: SPLASH includes OOPSLA |
Internet address |
Keywords
- Program verification
- Parallel programming
- MPI
- Session types
- Dependent types