Inferring Types for Parallel Programs
Francisco Martins (LaSIGE, Faculty of Sciences, University of Lisbon),, Vasco Thudichum Vasconcelos (LaSIGE, Faculty of Sciences, University of, Lisbon), Hans H\"uttel (Department of Computer Science, Aalborg University)
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.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.