Choreographies, Divided and Conquered

Luís Cruz-Filipe, Fabrizio Montesi [2016].
In CoRR abs/1602.03729.

Abstract

A recent study of bugs in real-world concurrent and distributed systems found that, while implementations of individual protocols tend to be robust, the composition of multiple protocols and its interplay with internal computation is the culprit for most errors. Multiparty Session Types and Choreographic Programming are methodologies for developing correct-by-construction concurrent and distributed software, based on global descriptions of communication flows. However, protocol composition is either limited or left unchecked. Inspired by these two methodologies, in this work we present a new language model for the safe composition of protocols, called Procedural Choreographies (PC). Protocols in PC are procedures, parameterised on the processes that enact them. Procedures define communications declaratively using global descriptions, and programs are written by invoking and composing these procedures. An implementation in terms of a process model is then mechanically synthesised, guaranteeing correctness and deadlock-freedom. We study PC in the settings of synchronous and asynchronous communications, and illustrate its expressivity with some representative examples.

Links

arxiv.org

Additional notes

None

Cite (BibTeX)

Click to expand

@article{DBLP:journals/corr/Cruz-FilipeM16,
  author       = {Lu{\'{\i}}s Cruz{-}Filipe and
                  Fabrizio Montesi},
  title        = {Choreographies, Divided and Conquered},
  journal      = {CoRR},
  volume       = {abs/1602.03729},
  year         = {2016},
  url          = {http://arxiv.org/abs/1602.03729},
  eprinttype    = {arXiv},
  eprint       = {1602.03729},
  timestamp    = {Mon, 13 Aug 2018 16:48:45 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/Cruz-FilipeM16.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

Peer-reviewed version

Click to show in publication list