That's Enough: Asynchrony with Standard Choreography Primitives

TL;DR

This paper demonstrates that standard choreography primitives are sufficient to model asynchronous communications in distributed systems, eliminating the need for ad-hoc extensions and simplifying reasoning about real-world systems.

Contribution

It shows how existing choreography calculus can encode asynchrony using process spawning and name mobility, avoiding complex extensions.

Findings

Standard choreography calculus can encode message in transit.

Asynchronous communication can be reasoned about without ad-hoc syntax.

Simplifies modeling of real-world distributed systems.

Abstract

Choreographies are widely used for the specification of concurrent and distributed software architectures. Since asynchronous communications are ubiquitous in real-world systems, previous works have proposed different approaches for the formal modelling of asynchrony in choreographies. Such approaches typically rely on ad-hoc syntactic terms or semantics for capturing the concept of messages in transit, yielding different formalisms that have to be studied separately. In this work, we take a different approach, and show that such extensions are not needed to reason about asynchronous communications in choreographies. Rather, we demonstrate how a standard choreography calculus already has all the needed expressive power to encode messages in transit (and thus asynchronous communications) through the primitives of process spawning and name mobility. The practical consequence of our results is that we can reason about real-world systems within a choreography formalism that is simpler than those hitherto proposed.