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.

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.

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