Formal Specification of the MPI-2.0 Standard in TLA+

School of Computing, University of Utah

Overview

This TLA+ model represents the first formalization of a very large subset of MPI-2.0. It extends our previous work, in which we captured around 10% of the MPI-1.0 primitives.

MPI-TLA+ Specification

MPI TLA+ Specification (PDF | TAR)

The Journal Version

A Formal Specification of MPI 2.0

Papers

Formal Specification of the MPI-2.0 Standard in TLA+

Semantics Driven Partial-order Reduction for MPI-based Parallel Programs

An Approach to Formalization and Analysis of Message Passing Libraries

Visuals

Poster (PDF | PPT)