A model for correlation-based choreographic programming

Saverio Giallorenzo, Fabrizio Montesi, Maurizio Gabbrielli [2024].
In PeerJ Comput. Sci. 10.

Abstract

Choreographies provide a clear way to specify the intended communication behaviour of concurrent and distributed systems. Previous theoretical work investigated the translation of choreographies into (models of) programs based on message passing. However, existing theories still present a gap between how they model communications—using channel names à la CCS or $\pi$-calculus—and implementations—which use lower-level mechanisms for message routing. We start bridging this gap with a new formal framework called Applied Choreographies. In Applied Choreographies, developers write choreographies in a familiar syntax (from previous work) and reason about their behaviour through simple, abstract name-based communication semantics. The framework offers state-of-the-art features of choreographic models, e.g., modular programming supported via choreographic types. To provide its correctness guarantee, Applied Choreographies comes with a compilation procedure that transforms a choreography into a low-level, implementation-adherent calculus of Service-Oriented Computing (SOC). To manage the complexity of the compilation, we divide its formalisation and proof into three stages, respectively dealing with: (a) the translation of name-based communications into their SOC equivalents, namely, using correlation mechanisms based on message data; (b) the projection of the given choreography into a composition of partial, single-participant choreographies (towards their translation into SOC processes); (c) the translation of partial choreographies and the distribution of global, choreography-level state into local SOC processes. We provide behavioural correspondence results for each stage. Thus, given a choreography specification, we guarantee to synthesise its faithful service-oriented implementation.

Links

doi.org

Additional notes

None

Cite (BibTeX)

Click to expand

@article{DBLP:journals/peerj-cs/GiallorenzoMG24,
  author       = {Saverio Giallorenzo and
                  Fabrizio Montesi and
                  Maurizio Gabbrielli},
  title        = {A model for correlation-based choreographic programming},
  journal      = {PeerJ Comput. Sci.},
  volume       = {10},
  pages        = {e1907},
  year         = {2024},
  url          = {https://doi.org/10.7717/peerj-cs.1907},
  doi          = {10.7717/PEERJ-CS.1907},
  timestamp    = {Mon, 03 Mar 2025 22:20:26 +0100},
  biburl       = {https://dblp.org/rec/journals/peerj-cs/GiallorenzoMG24.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}