Supervisors

Suitable for

Abstract

Prerequisites: Concurrency and concurrent programming languages. Familiarity with Rust would be beneficial.

 

Background

Include:

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

Session types [1, 2] provide a formalism to statically verify that parallel programs are free of deadlock and other inconsistencies. Multiparty session types (MPST) are session types involving any number of participants, and describe the interactions of all participants together using global session types. Global types are projected for each participant to obtain a local protocol that the participant must follow. However, if a protocol contains branching, this projection can be undefined.

Focus

Include:

• Research topic/question and expected contribution.

In this project you will investigate whether it is possible to modify a concurrent protocol that would not otherwise be projectable, to one that is, and establish any performance cost of this.

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.

You will modify a protocol such that it is projectable, and implement this modified version. You will benchmark the performance cost of your approach. Further work includes improving on your initial algorithm, and offering proofs that some set of otherwise-unprojectable protocols can be modified to be projected, along with the algorithmic complexity of this modification. You will implement code in Rust.

[1] 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.

[2] 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.