Supervisors

Suitable for

Abstract

Prerequisites:  Concurrent Programming. Lambda calculus and types, and familiarity with dependent and linear types would be advantageous but not required

Background

Include:

• A brief motivation for why the project is interesting.
• A summary of the area.

MPI [1, 2] is a widely used message-passing protocol for parallel computing used, for example, in exascale computing. Whilst powerful, MPI can still be used to write programs with deadlock and other concurrency bugs. To prevent this, we can use session types [3, 4] to statically verify parallel programs. Typically, type soundness is established, at least in part, outside the program used to implement concurrency. In this project, we aim to use recent developments in type theory to unify the programming language and concurrency verification.

Focus

Include:

• Research topic/question and expected contribution.

In this project, you'll expose a concurrency API in Idris that conforms to the MPI protocol, whilst ensuring soundness via Idris’ type system. Idris [5] is a functional programming language with dependent and linear types.

Method

Include:

• References to any papers, libraries or projects which might be used as a starting point.
• List of goals including which goals are essential to the project and which are stretch-goals.

We expect all students to create well-typed bindings for MPI, providing a synchronous API for binary sessions, with a basic set of MPI operations (send and recv, for example). We do not expect students to implement concurrency primitives themselves, but rather to create bindings to an existing implementation. Further work could extend this with: multiparty sessions; asynchronous communication; more interesting MPI operations.

[1] ‘MPI: A Message-Passing Interface Standard’, 2 November 2023. https://www.mpi-forum.org/docs/mpi-4.1/mpi41-report.pdf.

[2] Eijkhout, Victor. Parallel Programming in MPI and OpenMP. Vol. 2. The Art of HPC, 2022. https://theartofhpc.com/pcse.html.

[3] Yoshida, Nobuko, and Lorenzo Gheri. ‘A Very Gentle Introduction to Multiparty Session Types’. In Distributed Computing and Internet Technology, edited by Dang Van Hung and Meenakshi D´Souza, 11969:73–93. Lecture Notes in Computer Science. Cham: Springer International Publishing, 2020. https://doi.org/10.1007/978-3-030-36987-3_5.

[4] Coppo, Mario, Mariangiola Dezani-Ciancaglini, Luca Padovani, and Nobuko Yoshida. ‘A Gentle Introduction to Multiparty Asynchronous Session Types’. In Formal Methods for Multicore Programming, edited by Marco Bernardo and Einar Broch Johnsen, 9104:146–78. Lecture Notes in Computer Science. Cham: Springer International Publishing, 2015. https://doi.org/10.1007/978-3-319-18941-3_4.

[5] Brady, Edwin. ‘Idris 2: Quantitative Type Theory in Practice’. arXiv, 1 April 2021. http://arxiv.org/abs/2104.00480.