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.
2020
Computer Science - Software Engineering
Computer Science - Software Engineering
Computer Science - Logic in Computer Science
File in questo prodotto:
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.12571/10221
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? ND
social impact