| Summary: | 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.
|
|---|