Multiparty Session Types for Safe Runtime Adaptation in an Actor Language (Extended version)

TL;DR

This paper introduces EnsembleS, an actor-based language with a static session type system that enables safe runtime adaptation by verifying protocol compatibility during component discovery and replacement.

Contribution

It presents the design, implementation, and formal safety proof of EnsembleS, integrating multiparty session types with explicit connection actions for adaptive distributed systems.

Findings

EnsembleS supports safe runtime component replacement.

The type system guarantees communication safety for adaptive programs.

Application to an adaptive DNS server demonstrates practical effectiveness.

Abstract

Human fallibility, unpredictable operating environments, and the heterogeneity of hardware devices are driving the need for software to be able to adapt as seen in the Internet of Things or telecommunication networks. Unfortunately, mainstream programming languages do not readily allow a software component to sense and respond to its operating environment, by discovering, replacing, and communicating with components that are not part of the original system design, while maintaining static correctness guarantees. In particular, if a new component is discovered at runtime, there is no guarantee that its communication behaviour is compatible with existing components. We address this problem by using multiparty session types with explicit connection actions, a type formalism used to model distributed communication protocols. By associating session types with software components, the discovery process can check protocol compatibility and, when required, correctly replace components without jeapordising safety. We present the design and implementation of EnsembleS, the first actor-based language with adaptive features and a static session type system, and apply it to a case study based on an adaptive DNS server. We formalise the type system of EnsembleS and prove the safety of well-typed programs, making essential use of recent advances in non-classical multiparty session types.