Session Types for Reliable Distributed Systems (STARDUST)

VISON分布式软件系统是现代社会基础设施的重要组成部分。这种系统通常包括跨主机网络部署的各种软件组件。由于软件组件必须正确地彼此通信和同步，并且任何硬件或软件组件都可能出现故障，因此确保它们的可靠性是具有挑战性的。据估计，软件故障和服务中断每年给世界经济造成超过1万亿美元的损失。故障可能发生在系统堆栈的所有级别：硬件、操作系统、网络、软件和用户。在这里，我们重点介绍如何使用高级编程语言技术，使软件级别能够结合故障预防和容错来更好地处理故障。具体地说，我们将结合会话类型的通信结构化机制和基于参与者的软件体系结构的可扩展性和容错性，参与者语言基于通过异步消息进行通信的独立进程(参与者)。具有隔离状态的参与者有助于提高可靠性，因此参与者可以独立失败。在演员语言中实现可靠性的两个关键技术是超时和监督，这是Stardust的主要关注点。超时允许在执行期间识别故障，并通过在代码中建立触发器和替代行为来处理故障。参与者可以监督其他参与者，检测故障并采取补救措施，如重新启动失败的参与者。会话类型提供了一种指定和约束系统中节点之间的通信行为(协议)的方法。会话类型系统排除任何不一致的行为，可能是静态的(用于故障预防)、动态的或两者的混合(用于容错)。几种语言现在通过库和工具支持会话类型。通过结合参与者语言和会话类型的优势，我们将开发出具有明确定义的通信结构的可靠参与者编程的可靠理论。主要目标是交付为开发人员提供轻量级支持的工具，例如警告潜在问题，并允许开发人员继续使用已建立的习惯用法。通过这样做，我们的目标是在可靠的分布式软件系统的工程中实现一步的改变。

VISIONDistributed 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. Software failure and service outage are estimated to cost the world economy more than a trillion dollars annually.Failures can occur at all levels of the system stack: hardware, operating system, network, software, and user. Here we focus on using advanced programming language technologies to enable the software level to better handle failures using a combination of fault prevention and fault tolerance. Specifically, we will combine the communication-structuring mechanism of session types with the scalability and fault-tolerance of actor-based software architectures.Actor languages are based on independent processes (actors) communicating by asynchronous messages. Reliability is facilitated by actors having isolated state, and hence an actor can fail independently. Two key techniques for achieving reliability in actor languages are timeouts and supervision, and these are the main focus of STARDUST. Timeouts allow failures to be identified during execution, and failures are handled by establishing triggers and alternative behaviours within the code. An actor may supervise other actors, detecting failures and taking remedial action like restarting a failed actor.Session types provide a way to specify and constrain the communication behaviour (protocol) between nodes in a system. A session type system excludes any non-conforming behaviour, perhaps statically (for fault prevention), dynamically, or a mixture of both (for fault tolerance). Several languages now have session-type support via libraries and tools.By combining the strengths of actor languages and session types, we will develop a well-founded theory of reliable actor programming with clearly defined communication structures. Key aims are to deliver tools that provide lightweight support for developers, e.g. warn 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.