On Resolving Non-determinism in Choreographies

TL;DR

This paper introduces a new concept called whole-spectrum implementation that allows choreographies to have non-deterministic choices while ensuring their implementations are deterministic, improving correctness in message-passing systems.

Contribution

It proposes a formal notion of realisability for choreographies with non-deterministic choices and provides a type discipline to verify such implementations.

Findings

The notion of whole-spectrum implementation distinguishes between non-deterministic choreographies and deterministic implementations.

A type discipline is developed to check the correctness of implementations under this new notion.

Case study on the POP protocol demonstrates the applicability of the approach.

Abstract

Choreographies specify multiparty interactions via message passing. A realisation of a choreography is a composition of independent processes that behave as specified by the choreography. Existing relations of correctness/completeness between choreographies and realisations are based on models where choices are non-deterministic. Resolving non-deterministic choices into deterministic choices (e.g., conditional statements) is necessary to correctly characterise the relationship between choreographies and their implementations with concrete programming languages. We introduce a notion of realisability for choreographies - called whole-spectrum implementation - where choices are still non-deterministic in choreographies, but are deterministic in their implementations. Our notion of whole spectrum implementation rules out deterministic implementations of roles that, no matter which context they are placed in, will never follow one of the branches of a non-deterministic choice. We give a type discipline for checking whole-spectrum implementations. As a case study, we analyse the POP protocol under the lens of whole-spectrum implementation.