1. Allows designers to gain intuitions beyond that of a natural language description,
2. Dispels ambiguity,
3. Forces all assumptions to be made explicit, and
4. Can be used in concert with a model checker to determine when a sequence of interactions can lead to an error state.

In our paper (currently under review) we describe a formal model of MPI process interaction, detailing the protocols used in its implementation, and how it was validated using examples from the MPI standard document. We also demonstrate how a programmer might use the model to find bugs in their code, as well as gain a deeper understanding of the MPI standard itself. 

The model (in +CAL) can be downloaded from our website. 

We use the TLC model checker from Microsoft Research for this work.

• Discovery and analysis of program errors such as deadlock, message races, misuse of the MPI library and other errors.
• Automatic synthesis and transformation of synchronous programs into asynchronous programs including removal of barriers and discovery of intended collective operations.
• Formal specification of the MPI standard.