POST: Protocols, Observabilities and Session Types
Lead Research Organisation:
UNIVERSITY OF OXFORD
Department Name: Computer Science
Abstract
Communication is not only an essential organisation principle for emerging large-scale distributed applications, such as those for e-Commerce, e-Science, e-Healthcare and financial technology (FinTech): it is also an effective way to use computational resources, such as microservices and manycore chips. In this new paradigm, communication and concurrency are the norm in software development rather than a marginal concern, enabling architects and programmers to harness the power of hundreds or even thousands of concurrent processes interacting through *message passing*.
However, for this paradigm there is no well-established methodology for software development with safety and security gurantee based on clear and mathematically accurate criteria on its behaviour. This leaves uncertainty on the correctness of the construction of distributed infrastructure. The aim of this fellowship is to establish general and practical foundations for safety enforcement of communication-intensive concurrent and distributed applications, building on a general theory of *multiparty session types*.
Communications in a distributed application are commonly organised into multiple structured conversations (*protocols*) where a developer or programmer wishes to enforce *observabilities* of system behaviours to follow a safety and security criteria given by a protocol. Here *observability* of systems behaviours means a visible sequence of message exchanges with more complex information such as dependency of data, secure information, cost and timing of communications. In the multiparty session types, an end-point system properly carries out its responsibility, so that observable systems behaviours as a whole obey an agreed-upon protocol.
Multiparty session types articulate the basic dynamics in a respective computing paradigm, thus serving as a foundation for modelling, specification, verification, systematic testing and certification, enhanced with other methods such as monitoring and logical assertions. This fellowship aims to fulfil this potential of multiparty session types as types for communication by carrying out experiments. To achieve this goal, the following technical objectives have been identified:
1. The establishment of a uniform type theory for multiparty session types capturing a full range of application-level protocols based on behavioural theory and game semantics, as a foundation of the whole methodology.
2. The establishment of a dependent and refinement type theory of specifications and verifications; and of a scalable algorithm to verify safety and security properties based on automata theory.
3. The development and release of an open-source toolchain, based on (1,2), combined with Application Programming Interface (API) and with industry tools.
4. A theoretically well-founded architecture which can efficiently monitor, trace, log and enforce correct observational behaviour against specifications written in (3).
5. Experiments through collaboration with academic and industry partners, realising formal safety and security assurance against advanced protocols for real-world applications, including multi robotics/UAVs, financial and healthcare systems.
Throughout the research programme, an active and extensive dialogue between theories (1,2) and practice (3,4,5) will be the key enabler for reaching the goals of the fellowship, ultimately establishing cross-disciplinary and co-created ICT research. The project also links assurance methodologies based on session types to the standardisation for Cloud Computing (Cloud Native Computing Foundation) and to the public regulatory requirements for the documentation of financial and e-Healthcare protocols, meeting the goals of People at the Heart of ICT.
However, for this paradigm there is no well-established methodology for software development with safety and security gurantee based on clear and mathematically accurate criteria on its behaviour. This leaves uncertainty on the correctness of the construction of distributed infrastructure. The aim of this fellowship is to establish general and practical foundations for safety enforcement of communication-intensive concurrent and distributed applications, building on a general theory of *multiparty session types*.
Communications in a distributed application are commonly organised into multiple structured conversations (*protocols*) where a developer or programmer wishes to enforce *observabilities* of system behaviours to follow a safety and security criteria given by a protocol. Here *observability* of systems behaviours means a visible sequence of message exchanges with more complex information such as dependency of data, secure information, cost and timing of communications. In the multiparty session types, an end-point system properly carries out its responsibility, so that observable systems behaviours as a whole obey an agreed-upon protocol.
Multiparty session types articulate the basic dynamics in a respective computing paradigm, thus serving as a foundation for modelling, specification, verification, systematic testing and certification, enhanced with other methods such as monitoring and logical assertions. This fellowship aims to fulfil this potential of multiparty session types as types for communication by carrying out experiments. To achieve this goal, the following technical objectives have been identified:
1. The establishment of a uniform type theory for multiparty session types capturing a full range of application-level protocols based on behavioural theory and game semantics, as a foundation of the whole methodology.
2. The establishment of a dependent and refinement type theory of specifications and verifications; and of a scalable algorithm to verify safety and security properties based on automata theory.
3. The development and release of an open-source toolchain, based on (1,2), combined with Application Programming Interface (API) and with industry tools.
4. A theoretically well-founded architecture which can efficiently monitor, trace, log and enforce correct observational behaviour against specifications written in (3).
5. Experiments through collaboration with academic and industry partners, realising formal safety and security assurance against advanced protocols for real-world applications, including multi robotics/UAVs, financial and healthcare systems.
Throughout the research programme, an active and extensive dialogue between theories (1,2) and practice (3,4,5) will be the key enabler for reaching the goals of the fellowship, ultimately establishing cross-disciplinary and co-created ICT research. The project also links assurance methodologies based on session types to the standardisation for Cloud Computing (Cloud Native Computing Foundation) and to the public regulatory requirements for the documentation of financial and e-Healthcare protocols, meeting the goals of People at the Heart of ICT.
Planned Impact
This fellowship aims to establish the safety and security assurance principles for communication-intensive software based on session types. The outcomes, based on mathematically accurate criteria for communications, are likely to have deep and broad impacts on the information technology sector, and hence be of considerable benefit to society.
(1) Who might benefit from this research?
The immediate beneficiaries are the partners of this proposal and the application domains they are engaged in, i.e. micro/web-services, distributed containers, legacy code analysis, e-Science (robotics), e-Healthcare and financial technology. More generally, those engaged in the development of large-scale distributed applications will also benefit, ranging from global enterprise to infrastructure for public sectors (e.g. healthcare).
The second class of beneficiaries are those who build tools and environments for the runtime management of distributed tracing (observabilities of systems behaviours), including the middleware targeted to Cloud Computing. The validation algorithms and monitor/tracing architecture offer a comprehensive framework for (hybrid) static and runtime safety enforcement, with automatic or semi-automatic development-time verification.
The third beneficiaries are end-users and society as a whole, especially users of IT infrastructure developed in this fellowship proposal. Once the usability of the methodology is established, the new assurance methodology will lead to a comprehensive certification framework as a public standard. For example, distributed tracing is being standardised through the OpenTracing standard, a language-agnostic standard for distributed tracing, developed by the industry partner (Red Hat). Collaborations with Red Hat will have a large impact on establishing the link with two major open source projects, OpenTracing and Jaeger, part of the Cloud Native Computing Foundation (CNCF).
(2) How might they benefit from this research?
This fellowship project will produce a toolchain whose comprehensive support for software development and safety assurance will be tested through prominent real large-scale use cases with the project partners. The development and management experience with the partners will make our toolchain usable by professional developers (including architects, designers and programmers).
In the medium term, when associated development methods have reached sufficient maturity, it is possible for application providers who are using OpenTracing or GitOps to contribute to the enhancement of the toolchain or provide their own versions. Similarly the ecosystem of programming languages and APIs for protocols (i.e. Scribble framework developed) will be enriched by those working inside and outside academic institutions.
Finally the end-users will benefit from the use of safer services with a clear guarantee of their behaviour. Applications will enjoy enriched functionalities because more time and cost can be spent on new functions rather than maintenance and informal manual assurance. Such a trend will be accelerated when the competition in the software tools market for the development and assurance of communication-intensive software emerges (through DevOps), and will be further assisted by a public standard for software quality based on the proposed methodologies. This will ensure the safety of large-scale infrastructures such as financial networks, healthcare and robotics/UAVs, all of which offer critical services and knowledge to our society, and influencing the policy and regulator, putting People in the Heart of ICT.
(1) Who might benefit from this research?
The immediate beneficiaries are the partners of this proposal and the application domains they are engaged in, i.e. micro/web-services, distributed containers, legacy code analysis, e-Science (robotics), e-Healthcare and financial technology. More generally, those engaged in the development of large-scale distributed applications will also benefit, ranging from global enterprise to infrastructure for public sectors (e.g. healthcare).
The second class of beneficiaries are those who build tools and environments for the runtime management of distributed tracing (observabilities of systems behaviours), including the middleware targeted to Cloud Computing. The validation algorithms and monitor/tracing architecture offer a comprehensive framework for (hybrid) static and runtime safety enforcement, with automatic or semi-automatic development-time verification.
The third beneficiaries are end-users and society as a whole, especially users of IT infrastructure developed in this fellowship proposal. Once the usability of the methodology is established, the new assurance methodology will lead to a comprehensive certification framework as a public standard. For example, distributed tracing is being standardised through the OpenTracing standard, a language-agnostic standard for distributed tracing, developed by the industry partner (Red Hat). Collaborations with Red Hat will have a large impact on establishing the link with two major open source projects, OpenTracing and Jaeger, part of the Cloud Native Computing Foundation (CNCF).
(2) How might they benefit from this research?
This fellowship project will produce a toolchain whose comprehensive support for software development and safety assurance will be tested through prominent real large-scale use cases with the project partners. The development and management experience with the partners will make our toolchain usable by professional developers (including architects, designers and programmers).
In the medium term, when associated development methods have reached sufficient maturity, it is possible for application providers who are using OpenTracing or GitOps to contribute to the enhancement of the toolchain or provide their own versions. Similarly the ecosystem of programming languages and APIs for protocols (i.e. Scribble framework developed) will be enriched by those working inside and outside academic institutions.
Finally the end-users will benefit from the use of safer services with a clear guarantee of their behaviour. Applications will enjoy enriched functionalities because more time and cost can be spent on new functions rather than maintenance and informal manual assurance. Such a trend will be accelerated when the competition in the software tools market for the development and assurance of communication-intensive software emerges (through DevOps), and will be further assisted by a public standard for software quality based on the proposed methodologies. This will ensure the safety of large-scale infrastructures such as financial networks, healthcare and robotics/UAVs, all of which offer critical services and knowledge to our society, and influencing the policy and regulator, putting People in the Heart of ICT.
Organisations
- UNIVERSITY OF OXFORD (Lead Research Organisation)
- JPEX Ltd. (Project Partner)
- Estafet (Project Partner)
- Binghamton University (Project Partner)
- Max Planck Institutes (Project Partner)
- Weaveworks (Project Partner)
- ASTRAZENECA UK LIMITED (Project Partner)
- Red Hats Labs (Project Partner)
- Cognizant Technology Solutions (Project Partner)
Publications

Barbanera F
(2023)
Multicompatibility for Multiparty-Session Composition

Barwell A
(2023)
Designing Asynchronous Multiparty Protocols with Crash-Stop Failures

Barwell A
(2023)
Designing Asynchronous Multiparty Protocols with Crash-Stop Failures

Barwell A D
(2023)
Designing Asynchronous Multiparty Protocols with Crash-Stop Failures

Castro-Perez D
(2023)
Dynamically Updatable Multiparty Session Protocols (Artifact)



Gheri L
(2023)
Hybrid Multiparty Session Types -- Full Version

Gheri L
(2023)
Hybrid Multiparty Session Types: Compositionality for Protocol Specification through Endpoint Projection
in Proceedings of the ACM on Programming Languages
Related Projects
Project Reference | Relationship | Related To | Start | End | Award Value |
---|---|---|---|---|---|
EP/T006544/1 | 31/03/2020 | 29/09/2022 | £1,462,802 | ||
EP/T006544/2 | Transfer | EP/T006544/1 | 30/09/2022 | 30/03/2026 | £1,243,069 |
Description | We achieved the programming languages theories and practices for concurrency and communications based on session types. The PI's activities are recognised by various computer science filed. She obtained a Honorary Fellow at University of Glasgow. She obtained he third Suffrage Science Awards for Mathematics and Computing by London Institute of Medical Science (LMS) based on her scientific ans social contributions. Since the start of POST, 5 postdoctoral researchers in her group obtained permanent lectureships, professorships or research positions in top-rated universities in the UK, US, and Europe. Her leadership has led session types becoming one of the central topics in international conferences for Theoretical Computer Science and Programming Languages and Systems. In addition, her 4 papers were accepted in the leading programming systems conference, OOPSLA'20, breaking a record of the conference. She was awarded three best paper awards. She gave several keynote talks in various places such as FCT21 (Greece) and ST'30, |
Exploitation Route | The PI taught the courses related to the project at Imperial College London, University of Oxford, University of Keio and University of L'Aquila. The results are used in the toolboxes in TaRDIS (Horizon project) with four industry partners. |
Sectors | Communities and Social Services/Policy Digital/Communication/Information Technologies (including Software) Education Security and Diplomacy |
URL | https://mrg.cs.ox.ac.uk/ |
Description | The research developed in POST is going to be integrated into the toolbox of TaRDIS developed with Nova (Portugal), DTU (Denmark), Novi Sad (Servia), Athens (Greece), and other four companies. The toolbox enables to ensure the properties for communications such as deadlock-freedom and liveness propertis. Moreover, it enables to be extended to Federate Machine Learning. |
First Year Of Impact | 2023 |
Sector | Communities and Social Services/Policy,Digital/Communication/Information Technologies (including Software),Financial Services, and Management Consultancy,Security and Diplomacy |
Impact Types | Societal |
Title | Artifact: Deadlock-Free Asynchronous Message Reoerderign in Rust with Multiparty Session Types |
Description | Artifact of the paper: "Deadlock-Free Asynchronous Message Reoerderign in Rust with Multiparty Session Types", PPoPP 2022. |
Type Of Technology | Software |
Year Produced | 2021 |
Open Source License? | Yes |
Impact | The Rumpsteak framework is a framework for MPST in Rust. This software is an artifact that shows its capabilities. |
URL | https://zenodo.org/record/5786034 |
Title | Artifact: Design-By-Contract for Flexible Multiparty Session Protocols |
Description | Artifact for the paper : Design-By-Contract for Flexible Multiparty Session Protocols |
Type Of Technology | Software |
Year Produced | 2022 |
Open Source License? | Yes |
Impact | Artifact supporting the paper : Design-By-Contract for Flexible Multiparty Session Protocols |
URL | https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.2.21 |
Title | Artifact: Dynamically Updatable Multiparty Session Protocols |
Description | Artifact for the paper: Dynamically Updatable Multiparty Session Protocols |
Type Of Technology | Software |
Year Produced | 2023 |
Open Source License? | Yes |
Impact | Artifact supporting the paper Dynamically Updatable Multiparty Session Protocols |
URL | https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.10 |
Title | Artifact: Generalised Multiparty Session Types with Crash-Stop Failures |
Description | Artifact supporting the paper : Generalised Multiparty Session Types with Crash-Stop Failures |
Type Of Technology | Software |
Year Produced | 2022 |
Open Source License? | Yes |
Impact | Artifact for the paper : https://github.com/alcestes/mpstk-crash-stop |
URL | https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.35 |
Title | Artifact: Generic Go to Go: Dictionary-Passing, Monomorphisation, and Hybrid |
Description | Artifact for paper: Generic Go to Go: Dictionary-Passing, Monomorphisation, and Hybrid |
Type Of Technology | Software |
Year Produced | 2022 |
Open Source License? | Yes |
Impact | Artifact for paper : Generic Go to Go: Dictionary-Passing, Monomorphisation, and Hybrid |
URL | https://dl.acm.org/doi/10.1145/3563331 |
Title | Artifact: Rollback Recovery in Session-Based Programming |
Description | Artifact for paper: Rollback Recovery in Session-Based Programming |
Type Of Technology | Software |
Year Produced | 2023 |
Impact | Artifact for paper: Rollback Recovery in Session-Based Programming |
URL | https://link.springer.com/chapter/10.1007/978-3-031-35361-1_11#chapter-info |
Title | Artifact: Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types |
Description | Artifact for the paper: Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types (https://doi.org/10.4230/DARTS.8.2.9) This introduces the `multicrusty` library. |
Type Of Technology | Software |
Year Produced | 2022 |
Open Source License? | Yes |
Impact | Artifact supporting the paper. |
URL | https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.2.9 |
Title | Designing Asynchronous Multiparty Protocols with Crash-Stop Failures (Artifact) |
Description | We introduce Teatrino, a toolchain that supports handling multiparty protocols with crash-stop fail- ures and crash-handling behaviours. Teatrino accompanies the novel MPST theory in the related article, and enables users to generate fault-tolerant protocol-conforming Scala code from Scribble protocols. Local types are projected from the global protocol, enabling correctness-by-construction, and are expressed directly as Scala types via the Effpi concurrency library. Teatrino extends both Scribble and Effpi with support for crash-stop behaviour. The generated Scala code is execut- able and can be further integrated with existing systems. The accompanying theory in the related article guarantees deadlock-freedom and liveness properties for failure handling protocols and their implementation. This artifact includes examples, extended from both session type and distributed systems literature, featured in the related article. |
Type Of Technology | Software |
Year Produced | 2023 |
Open Source License? | Yes |
Impact | Artifact supporting the paper Designing Asynchronous Multiparty Protocols with Crash-Stop Failures |
URL | https://zenodo.org/record/7974824 |