Session Types for Reliable Distributed Systems (STARDUST)

Lead Research Organisation: University of Kent
Department Name: Sch of Computing

Abstract

Abstracts are not currently available in GtR for all funded research. This is normally because the abstract was not required at the time of proposal submission, but may be because it included sensitive information such as personal details.
 
Description (1) A model of grey failures for actor-based systems.

We have provided a formal model of actor systems with grey failures. The model allows us to better understand the (complex) nature of grey failures, and defines the problem space for the study of recoverability in real-world systems. The work ventures into the study of more complex failures than `fail-stop' failures, and considers more complex patters such as partial and temporary failures, while setting realistic assumptions as to the knowledge of the state of health of the system. In our model, the parts of the system do not have awareness on which failures are actually affecting a system at a certain time, and are only able to make judgments on the basis of their observation (e.g, missed deadlines). We reduced the problem of checking failures-tolerance to the problem of comparing behaviour of two systems, using the well-known notion of bisimulation. We gave different definitions of recoverability, all reduced to instances of checking bisimulation.
This key finding completes the project's objective O1.1.
Exploitation Route The model can be used as a reference pint in the understanding of gray failures by other researchers.

This work paves the path to promising developments: automated verification of fault-tolerance
of a system with respect to a set of failures, and characterization of the set of failures a system can handle.
To practically enable this, the model can be encoded into existing model checkers. For example, we have a prototype
encoding in an existing model checker called UPAAL.

Initial exploration of concrete links with programming languages are promising, also thanks to the close relationship of the model to
the programming features of the Erlang programming language. The model (once verified) can be used to generate code (e.g, in Erlang statem), or even tests (e.g., for Erlang via QuickCheck).
Sectors Digital/Communication/Information Technologies (including Software),Education
URL https://link.springer.com/chapter/10.1007/978-3-031-08143-9_9
 
Description 1) Our theory for protocol composition, which enables semi-automated composition of protocols expressed as e.g., session types, is implemented in a tool that enables code generation and model extraction. A preliminary version of the work was demonstrated, upon invitation, in two developers conferences (CodeMesh 20 and CodeBeam 21). The main impact is to enable communication with practitioners, advocating development techniques based on structured communications and session types, and demonstrate/assess potential of integration in common practices. The video of CodeBeam 21 is still available onYouTube and has 654 views (on 10/3/23) by the general audience. 2) Our model of failure has ignited interaction with project partners (Actyx and Quviq) at the latest Stardust Meeting (September 23) and during a secondment of Laura Bocchi to CodeBaker Ltd in Bologna, Italy. We have identified model extraction and testing as two major potential applications to look at. Both (1) and (2) have been used as teaching material in third-year BSc module COMP6610 (Theory and Practice of Concurrency) at the University of Kent.
First Year Of Impact 2020
Sector Digital/Communication/Information Technologies (including Software),Education
Impact Types Cultural
 
Description Global session types with asynchronous mixed choices 
Organisation Queen Mary University of London
Country United Kingdom 
Sector Academic/University 
PI Contribution Work on asynchronous session types and communicating automata normally forbids models featuring a construct called mixed choice (state where one can do both send and receive actions). This is to preserve safety of communications. On the other hand, mixed choices are a useful abstraction of very well known and used constructs like timeouts and deadlines. Timeouts are paramount to handle failures. We are proposing a variant of asynchronous session types that allows mixed choices in a safe, well-regulated manner, in order to extend expressiveness of the model while preserving safety guarantees.
Collaborator Contribution I am contributing to the global semantics and theoretical proofs. Ray Hu (Queen Mary) is contributing to realizing the global semantics as a distributed model and to developing a tool to validate the theory and allow for impact. Laura Voinea (University of Glasgow) is contributing to the general development and to collection of use cases.
Impact Work to be submitted to top conference of concurrency theory in Spring 2023.
Start Year 2022
 
Description Global session types with asynchronous mixed choices 
Organisation University of Glasgow
Country United Kingdom 
Sector Academic/University 
PI Contribution Work on asynchronous session types and communicating automata normally forbids models featuring a construct called mixed choice (state where one can do both send and receive actions). This is to preserve safety of communications. On the other hand, mixed choices are a useful abstraction of very well known and used constructs like timeouts and deadlines. Timeouts are paramount to handle failures. We are proposing a variant of asynchronous session types that allows mixed choices in a safe, well-regulated manner, in order to extend expressiveness of the model while preserving safety guarantees.
Collaborator Contribution I am contributing to the global semantics and theoretical proofs. Ray Hu (Queen Mary) is contributing to realizing the global semantics as a distributed model and to developing a tool to validate the theory and allow for impact. Laura Voinea (University of Glasgow) is contributing to the general development and to collection of use cases.
Impact Work to be submitted to top conference of concurrency theory in Spring 2023.
Start Year 2022
 
Description Model of grey failures for actor-based systems 
Organisation Royal Holloway, University of London
Country United Kingdom 
Sector Academic/University 
PI Contribution I (PI at Kent) have contriobuted with expertise on times semantics. Simon Thompson (Co-I at Kent) has contributed with expertise on failure recovery in actor-based systems and in particular Erlang. Laura Voinea (RA at Kent until March 2022 and now external contributor at University of Glasgow) has contributed with her time and expertise. All have contributed to joined effort towards producing a model of grey failures. Currently we are working towards publication on a journal (Logical Methods in Computer Science).
Collaborator Contribution Julien Lange (Royal Holloway) has contributed with his expertise on model checking and concurrency to joined effort towards producing a model of grey failures. Laura Voinea (University of Glasgow since March 2022) has contributed with examples and proofs of concept.
Impact A model of grey failures for actor-based systems. The work is the first work that proposes a characterization and analysis method for grey failures based on process algebras. We presented a notion of equivalence between systems affected by failures. One of the novelties is that our equivalence is for mailbox-based communications (used in actor-based systems) and this allows us to model complex real-life examples like the Circuit-Breaker and Producer-Consumer patterns. We reduced the problem of checking reliability properties (resilience, recoverability, augmentation of recovery strategies) in terms of bisimulation. This work has been presented in Dagstuhl seminar (and published in corresponding report 21372), presented at AGERE 2021, and published and presented at COORDINATION 2022. The work was invited for the COORDINATION 2022 special issue on the journal Logical Methods on Computer Science and is currently under review.
Start Year 2020
 
Description Model of grey failures for actor-based systems 
Organisation University of Glasgow
Country United Kingdom 
Sector Academic/University 
PI Contribution I (PI at Kent) have contriobuted with expertise on times semantics. Simon Thompson (Co-I at Kent) has contributed with expertise on failure recovery in actor-based systems and in particular Erlang. Laura Voinea (RA at Kent until March 2022 and now external contributor at University of Glasgow) has contributed with her time and expertise. All have contributed to joined effort towards producing a model of grey failures. Currently we are working towards publication on a journal (Logical Methods in Computer Science).
Collaborator Contribution Julien Lange (Royal Holloway) has contributed with his expertise on model checking and concurrency to joined effort towards producing a model of grey failures. Laura Voinea (University of Glasgow since March 2022) has contributed with examples and proofs of concept.
Impact A model of grey failures for actor-based systems. The work is the first work that proposes a characterization and analysis method for grey failures based on process algebras. We presented a notion of equivalence between systems affected by failures. One of the novelties is that our equivalence is for mailbox-based communications (used in actor-based systems) and this allows us to model complex real-life examples like the Circuit-Breaker and Producer-Consumer patterns. We reduced the problem of checking reliability properties (resilience, recoverability, augmentation of recovery strategies) in terms of bisimulation. This work has been presented in Dagstuhl seminar (and published in corresponding report 21372), presented at AGERE 2021, and published and presented at COORDINATION 2022. The work was invited for the COORDINATION 2022 special issue on the journal Logical Methods on Computer Science and is currently under review.
Start Year 2020
 
Description Protocol engineering and code generation in Erlang 
Organisation University of Kent
Country United Kingdom 
Sector Academic/University 
PI Contribution I (PI at Kent) contributed with the ideas and led the research.
Collaborator Contribution Laura Voinea (RA at Kent for STARDUST), and Dominic Orchard (collaborator at the University of Kent) contributed with their work and expertise. Laura Voinea contributed to the tool and presentation. Dominic contributed to the proofs, tool, and presentation.
Impact Theory of protocol composition with tool that allows composition and code generation for Erlang. Presented at two major developers conferences: Code Mesh V 2020, and Code Beam V 2021. Published in journal: The Art, Science, and Engineering of Programming, 2023. To be presented at held in Tokyo in March 2023.
Start Year 2020
 
Description Timed reversible computing 
Organisation Nagoya University
Country Japan 
Sector Academic/University 
PI Contribution I brought in my expertise about timed semantics and failures, and time into producing a joint seminal work that brings together time and reversibility.
Collaborator Contribution Prof Ivan Lanese (University of Bologna, Italy) and Prof Claudio Mezzina (University of Urbino, Italy) brought in their expertise on reversibility and debugging, while Prof Shoji Yuen (Nagoya University, Japan) brought in his expertise on real-time systems. All collaborators contributed with their time into producing a joint seminal work that brings together time and reversibility.
Impact We produced a seminal work on the inter-relations of reversibility and time. This is crucial to define well-funded checkpointing and recovery, as well as to improve debugging of real-world scenarios. The work was accepted for publication and presentation at FORTE 2022, and invited for the FORTE 2022 special issue in the journal Logical Methods of Computer Science. The journal version has been submitted and is currently under review.
Start Year 2020
 
Description Timed reversible computing 
Organisation University of Bologna
Country Italy 
Sector Academic/University 
PI Contribution I brought in my expertise about timed semantics and failures, and time into producing a joint seminal work that brings together time and reversibility.
Collaborator Contribution Prof Ivan Lanese (University of Bologna, Italy) and Prof Claudio Mezzina (University of Urbino, Italy) brought in their expertise on reversibility and debugging, while Prof Shoji Yuen (Nagoya University, Japan) brought in his expertise on real-time systems. All collaborators contributed with their time into producing a joint seminal work that brings together time and reversibility.
Impact We produced a seminal work on the inter-relations of reversibility and time. This is crucial to define well-funded checkpointing and recovery, as well as to improve debugging of real-world scenarios. The work was accepted for publication and presentation at FORTE 2022, and invited for the FORTE 2022 special issue in the journal Logical Methods of Computer Science. The journal version has been submitted and is currently under review.
Start Year 2020
 
Description Timed reversible computing 
Organisation University of Urbino
Country Italy 
Sector Academic/University 
PI Contribution I brought in my expertise about timed semantics and failures, and time into producing a joint seminal work that brings together time and reversibility.
Collaborator Contribution Prof Ivan Lanese (University of Bologna, Italy) and Prof Claudio Mezzina (University of Urbino, Italy) brought in their expertise on reversibility and debugging, while Prof Shoji Yuen (Nagoya University, Japan) brought in his expertise on real-time systems. All collaborators contributed with their time into producing a joint seminal work that brings together time and reversibility.
Impact We produced a seminal work on the inter-relations of reversibility and time. This is crucial to define well-funded checkpointing and recovery, as well as to improve debugging of real-world scenarios. The work was accepted for publication and presentation at FORTE 2022, and invited for the FORTE 2022 special issue in the journal Logical Methods of Computer Science. The journal version has been submitted and is currently under review.
Start Year 2020
 
Description Tractable algorithms for comparing process behaviour 
Organisation Gran Sasso Science Institute, L'Aquila, Italy
Country Italy 
Sector Academic/University 
PI Contribution I, Andy King (RA at Kent) and Maurizio Murgia (external collaborator at Gran Sasso Science Institute) are developing algorithms to analyze the behaviour of distributed processes. We are addressing known undecidable problems, looking for semi-algorithm that extend the state of the art. Our methodology can be generalized to several application scenarios, not just distributed processes, and may impact different application areas.
Collaborator Contribution Provided insight and technical skills in developing and validating theory. The partner is implementing a tool to support theory development and validation, as well as facilitate impact and usability of results.
Impact We aim at two publications in spring 2023 in two top conferences of concurrency theory and verification.
Start Year 2022
 
Title Protocol composition and code generation in Erlang 
Description The software allows users to implement the composition of two or more application-level protocols (e.g., banking, pin-tan authentication). The generated compositions and implementations are guaranteed to be faithful to the original component protocols. Formally, the implemented notion of composition enjoys behaviour preservation (no behaviour is added to the original protocols) and fairness (no behaviour is neglected from the original protocols). This is guaranteed by the formal foundations of this tool (see https://kar.kent.ac.uk/93297/ for a report on the underlying theory. Concretely, the software allows the user to: - define application-level protocols, such as banking, pin-tan authentication. - automatically obtain composite protocols, such as banking with authentication. This is intended as an iterative process by which the user can steer compositions using assertions, and improves own awareness of the desired interleaving of the two component protocols. - automatically generate code (stubs) in Erlang that implement a given protocol composition. - migrate code between compositions. 
Type Of Technology Webtool/Application 
Year Produced 2021 
Impact The practicality of the (novel) theory on protocol composition was assessed and improved on the basis of this tool. The tool allows us to demonstrate the theory and its implications in two large developers conferences (Code Mesh 2020 and Code Beam 2021) and seminars, to gain feedback and improve the theory and tool usability. This prototype shows feasibility of an agile and less error-prone approach, based on techniques already used by programmers like assertions, to correct-by-construction implementations of concurrent software. 
URL https://kar.kent.ac.uk/93297/
 
Description Code Beam 2021 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact Invited presentation of work on protocol composition and code generation in Erlang to audience of practitioners at Code Beam 2021.
The event was a virtual event attended mostly by practitioners. The talk was belatedly released to the public by the organisers and is available on Youtube:
https://www.youtube.com/watch?v=VPW6H0L4Gek
The talk has about 386 views on Youtube (seen on 24/2/22).
Audience to the recording may include general public and students.
Year(s) Of Engagement Activity 2021
 
Description Code Mesh 2020 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact Presentation of work (talk and demo of over 30 minutes) on protocol composition and code generation in Erlang to an audience of practitioners to Code Mesh 2020.
The talk, besides being well attended during the event, was belatedly made public on Youtube by the organisers. My talk has 424 views (seen on 21/2/22), likely by practitioners, but members of general public and students. The talk can be found on Youtube at this link: https://www.youtube.com/watch?v=aWJ19RsGbWg&t=2026s

Following the interest raised by the talk, I was later invited to present the work (and its developments) to another developers conference: Code Beam 2021.
Year(s) Of Engagement Activity 2020
URL https://codesync.global/conferences/code-mesh-ldn/
 
Description Participation at Dagstuhl 23112 
Form Of Engagement Activity A formal working group, expert panel or dialogue
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Other audiences
Results and Impact This Dagstuhl Seminar seeks to enable conversations and solutions cutting across the deductive verification and model checking communities, leveraging the complementary strengths of these approaches. In particular, the seminar will explore layered and compositional approaches for modeling and verification of industrial-scale distributed systems that lend themselves well to separation of verification tasks, and thereby the use of diverse proof methodologies (from https://www.dagstuhl.de/en/seminars/seminar-calendar/seminar-details/23112)
Year(s) Of Engagement Activity 2023
URL https://www.dagstuhl.de/en/seminars/seminar-calendar/seminar-details/23112
 
Description Presentation at Dagstuhl 21372 
Form Of Engagement Activity A formal working group, expert panel or dialogue
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Other audiences
Results and Impact I and Laura Voinea (RA in the STARDUST project) presented our Model of Grey Failures as ongoing work, for discussion at Dagstuhl seminar series.
Dagstuhl seminars are a formal series of seminars, attended by invitation, attended by experts in specific topics.
In this case, the topic was "Behavioural Types: Bridging Theory and Practice".

There were more than 40 participants (some in person and some virtually), including one industry partner (Roland Kuhn, Actyx).

The seminar was attended also by participants to STARDUST from Imperial College and University of Glasgow.

Failure handling, the central topic of STARDUST, ended up being the central topic of this event.
Year(s) Of Engagement Activity 2021
URL https://www.dagstuhl.de/en/program/calendar/semhp/?semnr=21372
 
Description STARDUST meeting at Kent 
Form Of Engagement Activity A formal working group, expert panel or dialogue
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Other audiences
Results and Impact Project meeting involving partners from Imperial College London, University of Glasgow, University of Kent, industry partners Actyx and Quviq, and one external advisor (Ray Hu, Queen Mary London). The project was open and attended by postgraduate students at Kent and Imperial College London.
Year(s) Of Engagement Activity 2022
URL https://epsrc-stardust.github.io/meetings/kent22.html
 
Description Secondment to CodeBaker 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact Two one-week visits to italian software company CodeBaker, Bologna (Italy) and University of Bologna in the context of EU project BehAPI. During the meetings, overall, I discussed with three members of CodeBaker (CEO, marketing manager, and lead developer) and several stakeholders (about six) from the University of Bologna.

I presented a STARDUST work (1 hour seminar) about the model of grey failures we developed in WP1 of STARDUST and discussed fault tolerance as well as aspect of API design with the practitioners at CodeBaker.

CodeBaker provided us with API specifications use cases which we will use to assess out current modelling formalisms. They seemed keen in adopting a formalism for API specification (instead of using natural language). We discussed open problems related to fault-tolerance and hence STARDUST.
Year(s) Of Engagement Activity 2022,2023