ParTypes

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.

Team

Hugo Andrés López
César Santos
Vasco T. Vasconcelos
Eduardo R. B. Marques
Francisco Martins

 

Project

 

Downloads

ParTypes Eclipse plugin
Update Site
http://download.gloss.di.fc.ul.pt/ParTypes/eclipse-plugin
Requirements
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.

 

Learning ParTypes

Head over to the Online tutorial to learn and practice using ParTypes with no installation on your machine.

Publications

      • H. A. Lopéz and E. R. B. Marques and F. Martins and N. Ng and C. Santos and V. T. Vasconcelos and N. Yoshida , oopsla15 , Proc. OOPSLA’15 , ACM , ACM , OOPSLA’15 , 2015 (ParTypes-OOPSLA15)
      • Filipe Lemos , Synthesis of correct-by-construction MPI programs , MSc Thesis, Departamento de Informática, FCUL , DI/FCUL , 2014
         PEI.pdf
      • César Santos , Protocol-based programming of concurrent systems , MSc Thesis, Departamento de Informática, FCUL , DI/FCUL , 2014
         PEI.pdf
      • Vasco Thudichum Vasconcelos, Francisco Martins, Eduardo R. B. Marques, Hugo A. López, César Santos, and Nobuko Yoshida , Type-Based Verification of Message-Passing Parallel Programs , DI/FCUL , Dep. Informática Faculdade de Ciências da Universidade de Lisboa , 2014 (tr_types)
      • Eduardo R. B. Marques, Francisco Martins, Vasco T. Vasconcelos, César Santos, Nicholas Ng, Nobuko Yoshida , Protocol-based verification of MPI programs , Dep. Informática Faculdade de Ciências da Universidade de Lisboa , DI/FCUL , 2014
        tr_mpi.pdf
      • E.R.B. Marques and F. Martins and V.T. Vasconcelos and N. Ng and N. Martins , Towards deductive verification of MPI programs against session types , Post Proc. PLACES’13 , 2013 (places13)
      • N.D. Martins, C.Santos, E.R.B. Marques, F. Martins, V.T.Vasconcelos , Especificação e Verificação de Protocolos para Programas MPI , INFORUM , 2013 (inforum13)
      • Nuno Martins , Formal Verification of Parallel C+MPI Programs , MSc Thesis, Departamento de Informática, FCUL , DI/FCUL , 2013
        PEI.pdf
      • K. Honda, E.R.B. Marques, F. Martins, N. Ng, V.T. Vasconcelos, N. Yoshida , Verification of MPI programs using session types , Proc. EuroMPI 2012 , Springer , LNCS , 291-293 , 2012 (eurompi12)