Session Types for Reliable Distributed Systems (STARDUST)

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

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.