Choreographies, Divided and Conquered

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

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.
Additional notes
Cite (BibTeX)
Click to expand
  author       = {Lu{\'{\i}}s Cruz{-}Filipe and
                  Fabrizio Montesi},
  title        = {Choreographies, Divided and Conquered},
  journal      = {CoRR},
  volume       = {abs/1602.03729},
  year         = {2016},
  url          = {},
  eprinttype    = {arXiv},
  eprint       = {1602.03729},
  timestamp    = {Mon, 13 Aug 2018 16:48:45 +0200},
  biburl       = {},
  bibsource    = {dblp computer science bibliography,}

Peer-reviewed version
Click to show in publication list