Modular Compilation for Higher-Order Functional Choreographies

Luís Cruz-Filipe, Eva Graversen, Lovro Lugovic, Fabrizio Montesi, Marco Peressotti [2023].
In proceedings of ECOOP 2023, pp. 7:1-7:37.

Abstract

Choreographic programming is a paradigm for concurrent and distributed software, whereby descriptions of the intended communications (choreographies) are automatically compiled into distributed code with strong safety and liveness properties (e.g., deadlock-freedom).

Recent efforts tried to combine the theories of choreographic programming and higher-order functional programming, in order to integrate the benefits of the former with the modularity of the latter. However, they do not offer a satisfactory theory of compilation compared to the literature, because of important syntactic and semantic shortcomings: compilation is not modular (editing a part might require recompiling everything) and the generated code can perform unexpected global synchronisations.

In this paper, we find that these shortcomings are not mere coincidences. Rather, they stem from genuine new challenges posed by the integration of choreographies and functions: knowing which participants are involved in a choreography becomes nontrivial, and divergence in applications requires rethinking how to prove the semantic correctness of compilation.

We present a novel theory of compilation for functional choreographies that overcomes these challenges, based on types and a careful design of the semantics of choreographies and distributed code. The result: a modular notion of compilation, which produces code that is deadlock-free and correct (it operationally corresponds to its source choreography).

Links

doi.org

Additional notes

None

Cite (BibTeX)

Click to expand

@inproceedings{DBLP:conf/ecoop/Cruz-FilipeGLMP23,
  author       = {Lu{\'{\i}}s Cruz{-}Filipe and
                  Eva Graversen and
                  Lovro Lugovic and
                  Fabrizio Montesi and
                  Marco Peressotti},
  editor       = {Karim Ali and
                  Guido Salvaneschi},
  title        = {Modular Compilation for Higher-Order Functional Choreographies},
  booktitle    = {37th European Conference on Object-Oriented Programming, {ECOOP} 2023,
                  July 17-21, 2023, Seattle, Washington, United States},
  series       = {LIPIcs},
  volume       = {263},
  pages        = {7:1--7:37},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ECOOP.2023.7},
  doi          = {10.4230/LIPICS.ECOOP.2023.7},
  timestamp    = {Sat, 30 Sep 2023 09:39:31 +0200},
  biburl       = {https://dblp.org/rec/conf/ecoop/Cruz-FilipeGLMP23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

A PDF is available (possibly a preprint):