On Resolving Non-determinism in Choreographies

Choreographies specify multiparty interactions via message passing. Arealisation of a choreography is a composition of independent processes thatbehave as specified by the choreography. Existing relations ofcorrectness/completeness between choreographies and realisations are based onmodels where choices are non-deterministic. Resolving non-deterministic choicesinto deterministic choices (e.g., conditional statements) is necessary tocorrectly characterise the relationship between choreographies and theirimplementations with concrete programming languages. We introduce a notion ofrealisability for choreographies - called whole-spectrum implementation - wherechoices are still non-deterministic in choreographies, but are deterministic intheir implementations. Our notion of whole spectrum implementation rules outdeterministic implementations of roles that, no matter which context they areplaced in, will never follow one of the branches of a non-deterministic choice.We give a type discipline for checking whole-spectrum implementations. As acase study, we analyse the POP protocol under the lens of whole-spectrumimplementation.