A Theory of Available-by-Design Communicating Systems

TL;DR

This paper introduces a new choreographic programming calculus, GC_q, designed for distributed systems with dynamic component availability, ensuring correct and deadlock-free implementations despite failures.

Contribution

It develops the Global Quality Calculus (GC_q) with novel operators for failure-aware communication and provides a type system and endpoint projection methodology to handle dynamic availability.

Findings

GC_q supports multiparty, partial, and collective communications with failures.

A type system guarantees choreography realizability despite component failures.

Progress is maintained in well-typed choreographies with availability considerations.

Abstract

Choreographic programming is a programming-language design approach that drives error-safe protocol development in distributed systems. Starting from a global specification (choreography) one can generate distributed implementations. The advantages of this top-down approach lie in the correctness-by-design principle, where implementations (endpoints) generated from a choreography behave according to the strict control flow described in the choreography, and do not deadlock. Motivated by challenging scenarios in Cyber-Physical Systems (CPS), we study how choreographic programming can cater for dynamic infrastructures where not all endpoints are always available. We introduce the Global Quality Calculus ($GC_q$), a variant of choreographic programming for the description of communication systems where some of the components involved in a communication might fail. GCq features novel operators for multiparty, partial and collective communications. This paper studies the nature of failure-aware communication: First, we introduce $GC_q$ syntax, semantics and examples of its use. The interplay between failures and collective communications in a choreography can lead to choreographies that cannot progress due to absence of resources. In our second contribution, we provide a type system that ensures that choreographies can be realized despite changing availability conditions. A specification in $GC_q$ guides the implementation of distributed endpoints when paired with global (session) types. Our third contribution provides an endpoint-projection based methodology for the generation of failure-aware distributed processes. We show the correctness of the projection, and that well-typed choreographies with availability considerations enjoy progress.