# Inferring Types for Parallel Programs

## TL;DR

This paper introduces a type inference algorithm for MPI programs that automatically deduces communication protocols, ensuring deadlock freedom and aiding in the verification of parallel program correctness.

## Contribution

It presents a novel type inference method for a subset of the PARTYPES system, enabling static analysis of MPI programs to verify communication protocols.

## Key findings

- The algorithm successfully infers types from MPI source code.
- Well-typed programs are guaranteed to be deadlock-free.
- The approach enhances static verification of parallel programs.

## Abstract

The Message Passing Interface (MPI) framework is widely used in implementing imperative pro- grams that exhibit a high degree of parallelism. The PARTYPES approach proposes a behavioural type discipline for MPI-like programs in which a type describes the communication protocol followed by the entire program. Well-typed programs are guaranteed to be exempt from deadlocks. In this paper we describe a type inference algorithm for a subset of the original system; the algorithm allows to statically extract a type for an MPI program from its source code.

---
Source: https://tomesphere.com/paper/1704.03096