Session Types for Reliable Distributed Systems
Distributed software systems are an essential part of the infrastructure of modern society. Such systems typically comprise diverse software components deployed across networks of hosts. Ensuring their reliability is challenging, as software components must correctly communicate and synchronise with each other, and any of the hardware or software components may fail. Failure and service "outage" is extremely costly, with worldwide financial losses due to software failures in 2017 estimated at US$1.7tn, up from US$1.1tn in 2016.
Failures can occur at all levels of the system stack: hardware, operating systems, networks, software, and users. Here we focus on using advanced programming language technologies to enable the software level to handle failures that arise from any level of the stack. Our aim is to provide software-level reliability for distributed systems by combining fault prevention with fault tolerance. The key objective is to combine the communication-structuring mechanism of session types with the scalability and fault-tolerance of actor-based software architectures.
The result will be a well-founded theory of reliable actor programming, supported by a collection of libraries and tools, and validated on a range of case studies. Key aims are to deliver tools that provide lightweight support for developers – e.g. warning of potential issues – and to allow developers to continue to use established idioms. By doing so we aim to deliver a step change in the engineering of reliable distributed software systems.
STARDUST is funded by EPSRC (grants EP/T014512/1, EP/T014628/1, EP/T014709/1) between 1st October 2020 and 30th September 2024.
Approach.
The research approach of STARDUST is organised into three strands: Principles, Programming, and Practice.
Principles
We will develop foundational theories of reliable session types for distributed actor systems. Our models will capture the two prevalent means for failure recovery in actor-based languages: supervision trees and timeouts.
Programming
We will design, engineer and evaluate usable, open-source session type implementations and supporting tools for Erlang and Scala with Akka. We will develop type checking support for the enhanced session developed in the Principles strand, as well as a tool to help users to design session types for existing systems. These tools will be integrated with appropriate IDEs.
Practice
The theory and tools will be guided by, and evaluated against, a set of case studies provided by our industrial partners. The application domains are: industrial automation (Actyx); server engineering (Erlang Solutions); microservices (Lightbend); testing tools (Quviq); and organisation simulation (Tata).
Mailing Lists.
There are two mailing lists for STARDUST: stardust-announce, for announcements, and stardust-list, for more general discussion.
To subscribe, send an email to sympa@lists.cent.gla.ac.uk with the following in the Subject line:
SUB LISTNAME NAME
where LISTNAME
is one of stardust-announce or stardust-list, and NAME
is your first name followed by your last name.
To unsubscribe, send an email to sympa@lists.cent.gla.ac.uk with nothing in the Subject line. In the message body put the following:
UNSUBSCRIBE LISTNAME EMAIL
EMAIL
is an optional email address, useful if different from your "From:" address. If you normally have an automatic signature at the end of your email, please put the word QUIT
just before your signature.
People.
Glasgow
- Duncan Paul Attard (researcher)
- Simon Fowler (CoI)
- Simon Gay (PI)
- Danielle Marshall (Researcher)
- Phil Trinder (CoI)
Oxford
- Nobuko Yoshida (PI)
Kent
- Laura Bocchi (PI)
- Simon Thompson (CoI)
- Andy King (researcher)
Publications.
2024
- Laura Bocchi, Andy King and Maurizio Murgia. Asynchronous Subtyping by Trace Relaxation. TACAS 2024, to appear.
2023
- Simon Fowler, Duncan Paul Attard, Franciszek Sowul, Simon J. Gay, and Phil Trinder. Special Delivery: Programming with Mailbox Types. ICFP 2023.
- Jonah Pears, Laura Bocchi, and Andy King. Safe Asynchronous Mixed-Choice for Timed Interactions. COORDINATION 2023.
- Adam D. Barwell, Ping Hou, Nobuko Yoshida, and Fangyi Zhou. Designing Asynchronous Multiparty Protocols with Crash-Stop Failures. ECOOP 2023.
- Claudio Antares Mezzina, Francesco Tiezzi, and Nobuko Yoshida. Rollback Recovery in Session-Based Programming. COORDINATION 2023. (Best paper award)
- Simon Thompson and Dániel Horpácsi. Refactoring = Substitution + Rewriting: Towards Generic, Language-Independent Refactorings. Eelco Visser Commemorative Symposium, 2023.
2022
- Laura Bocchi, Dominic Orchard, and Laura Voinea. A Theory of Composing Protocols. The Art, Science, and Engineering of Programming (a preliminary version was presented at Code BEAM 2021 - video).
- Adam Barwell, Alceste Scalas, Nobuko Yoshida, and Fangyi Zhou. Generalised Multiparty Session Types with Crash-Stop Failures . CONCUR 2022.
- Laura Bocchi, Julien Lange, Simon Thompson, and Laura Voinea. A Model of Actors and Grey Failures. COORDINATION 2022.
- Laura Bocchi, Ivan Lanese, Claudio Antares Mezzina, and Shoji Yuen. The Reversible Temporal Process Language. FORTE 2022.
- Jose Cano and Phil Trinder P.W. (Eds) Euro-Par 2022: Parallel Processing, Proceedings of the 28th International Conference on Parallel and Distributed Computing (Euro-Par'22) Glasgow, UK Springer LNCS 13440 (August 2022).
- Aidan Randtoul and Phil Trinder A Reliability Benchmark for Actor-Based Server Languages Proceedings of the 21st ACM SIGPLAN International Workshop on Erlang (Erlang'22) Ljubljana, Slovenia (September 2022).
- Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. Stay Safe under Panic: Affine Rust Programming with Multiparty Session Types. ECOOP 2022.
- Ruomeng Xu, Anna Lito Michala and Phil Trinder CAEFL: Composable and Environment Aware Federated Learning Models Proceedings of the 21st ACM SIGPLAN International Workshop on Erlang (Erlang'22) Ljubljana, Slovenia (September 2022).
2021
- Paul Harvey, Simon Fowler, Ornela Dardha, and Simon J. Gay. Multiparty Session Types for Safe Runtime Adaptation in an Actor Language. ECOOP 2021.
- Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley, and J. Garrett Morris. Separating Sessions Smoothly. CONCUR 2021.