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.
The research approach of STARDUST is organised into three strands: Principles, Programming, and Practice.
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.
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.
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).
There are two mailing lists for STARDUST: stardust-announce, for announcements, and stardust-list, for more general discussion.
To subscribe, send an email to firstname.lastname@example.org with the following in the Subject line:
SUB LISTNAME NAME
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 email@example.com with nothing in the Subject line. In the message body put the following:
UNSUBSCRIBE LISTNAME EMAIL
QUITjust before your signature.
- 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)
- 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).
- 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.