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.
On Resolving Non-determinism in Choreographies
Emilio Tuosto
2020-01-01
Abstract
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.File | Dimensione | Formato | |
---|---|---|---|
2020_LogMethCompSci_16_Bocchi.pdf
accesso aperto
Tipologia:
Versione Editoriale (PDF)
Licenza:
Accesso gratuito
Dimensione
832.84 kB
Formato
Adobe PDF
|
832.84 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.