ParTypes is a toolchain for validating and synthesising message-based programs for Message Passing Interface (MPI) programs.
The general aim is to enforce program compliance with dependent-type based protocol specifications, enforcing properties such as protocol fidelity and the absence of deadlocks. The toolchain is composed of an Eclipse plug-in, an annotated MPI library, a C annotator, and makes use of the Verifying C Compiler (VCC), the Z3 SMT solver, and the Why3 platform.
A key result is that verification of C+MPI programs is immune to the state-explosion problem, and verification times are independent of input parameters such as the number of processes, contrasting with established methodologies for MPI program verification, e.g., employing model checking and/or symbol execution.
The Eclipse plug-in allows for the writing of protocol specifications, verifies that protocols are well formed (with the help of Z3 for checking dependent type restrictions), and generates protocol representations in VCC and WhyML formats for program verification. The plugin also synthesises C+MPI code programs that are correct-by-construction, also annotated with VCC logic that work as a proof of their correctness.
- MULTICORE – Advanced Type Systems for Multicore Programming
- Eclipse IDE Kepler or later installed (seems to be working with Neon and Java 8).
Installing the Z3 binaries
- Download the correct zip binaries for your Operative System (check the planed releases).
- Extract the archive and add the Z3 bin folder to your system path.
- Or clone the new Z3 repository and follow the instructions to compile it.
- Add the generated folder to the system path.
Installing the Eclipse ParTypes Plugin
- In Eclipse go to Preferences → Java → Installed JREs
- Press edit on the active JRE
- In Default VM arguments write -Djava.library.path=path/to/z3
- Go to the Help menu → Install New Software…
- Type in the update site in the work with field and press Enter;
- Select ParTypes Feature;
- Press the Next button;
- It takes a while for the update site to resolve the dependencies and contact the necessary update sites;
- Trust us and accept the unsigned plugin;
- Restart Eclipse. The installation is now complete.
Creating a ParTypes project
- In Eclipse go to File->New…->Project. Create a new MPI Sessions Project;
- A basic .prot file is automatically created;
- Write your program in the created .prot file. Here you can find some examples.
ParTypes VCC library
You will need the ParTypes VCC library to verify MPI programs against protocols generated by the Eclipse plugin. Download the latest version (0.8) here, then check
README.txt for some simple instructions of how to get started.
Head over to the Online tutorial to learn and practice using ParTypes with no installation on your machine.
- oopsla15 , Proc. OOPSLA’15 , ACM , ACM , OOPSLA’15 , 2015 (ParTypes-OOPSLA15) ,
- Synthesis of correct-by-construction MPI programs , MSc Thesis, Departamento de Informática, FCUL , DI/FCUL , 2014
- Protocol-based programming of concurrent systems , MSc Thesis, Departamento de Informática, FCUL , DI/FCUL , 2014
- Type-Based Verification of Message-Passing Parallel Programs , DI/FCUL , Dep. Informática Faculdade de Ciências da Universidade de Lisboa , 2014 (tr_types) ,
- Protocol-based verification of MPI programs , Dep. Informática Faculdade de Ciências da Universidade de Lisboa , DI/FCUL , 2014
- Towards deductive verification of MPI programs against session types , Post Proc. PLACES’13 , 2013 (places13) ,
- Especificação e Verificação de Protocolos para Programas MPI , INFORUM , 2013 (inforum13) ,
- Formal Verification of Parallel C+MPI Programs , MSc Thesis, Departamento de Informática, FCUL , DI/FCUL , 2013
- Verification of MPI programs using session types , Proc. EuroMPI 2012 , Springer , LNCS , 291-293 , 2012 (eurompi12) ,