Communications in choreographies, revisited

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

155 Downloads (Pure)

Abstract

Choreographic Programming is a paradigm for developing correct-by-construction concurrent programs, by writing high-level descriptions of the desired communications and then synthesising process implementations automatically. So far, choreographic programming has been explored in the monadic setting: interaction terms express point-to-point communications of a single value. However, real-world systems often rely on interactions of polyadic nature, where multiple values are communicated among two or more parties, like multicast, scatter-gather, and atomic exchanges.

We introduce a new model for choreographic programming equipped with a primitive for grouped interactions that subsumes all the above scenarios. Intuitively, grouped interactions can be thought of as being carried out as one single interaction. In practice, they are implemented by processes that carry them out in a concurrent fashion. After formalising the intuitive semantics of grouped interactions, we prove that choreographic programs and their implementations are correct and deadlock-free by construction.
Original languageEnglish
Title of host publicationProceedings of the 33rd Annual ACM Symposium on Applied Computing
PublisherAssociation for Computing Machinery
Publication date9. Apr 2018
Pages1248-1255
ISBN (Electronic)978-1-4503-5191-1/18/04
DOIs
Publication statusPublished - 9. Apr 2018
Event33rd Annual ACM Symposium on Applied Computing, SAC 2018 - Pau, France
Duration: 9. Apr 201813. Apr 2018

Conference

Conference33rd Annual ACM Symposium on Applied Computing, SAC 2018
Country/TerritoryFrance
CityPau
Period09/04/201813/04/2018
SponsorACM Special Interest Group on Applied Computing (SIGAPP)

Keywords

  • Choreography
  • Communication patterns
  • Concurrency
  • Programming languages
  • Formal methods
  • Semantics

Fingerprint

Dive into the research topics of 'Communications in choreographies, revisited'. Together they form a unique fingerprint.

Cite this