Communications in choreographies, revisited
Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti
[2018].
In proceedings of SAC 2018, pp. 1248-1255.
Choreographic Programming is a paradigm for developing correctby-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, realworld 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.
@inproceedings{DBLP:conf/sac/Cruz-FilipeMP18,
author = {Lu{\'{\i}}s Cruz{-}Filipe and
Fabrizio Montesi and
Marco Peressotti},
editor = {Hisham M. Haddad and
Roger L. Wainwright and
Richard Chbeir},
title = {Communications in choreographies, revisited},
booktitle = {Proceedings of the 33rd Annual {ACM} Symposium on Applied Computing,
{SAC} 2018, Pau, France, April 09-13, 2018},
pages = {1248--1255},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167132.3167267},
doi = {10.1145/3167132.3167267},
timestamp = {Wed, 25 Sep 2019 18:12:14 +0200},
biburl = {https://dblp.org/rec/conf/sac/Cruz-FilipeMP18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
A PDF is available (possibly a preprint):