Choral

A mainstream choreographic programming language.

website repository

Description

Choral is a language for the programming of choreographies. A choreography is a multiparty protocol that defines how some roles (the proverbial Alice, Bob, etc.) should coordinate with each other to do something together. At the press of a button, the Choral compiler translates a choreography into a library for each role. Choral makes sure that the compiled libraries are compliant implementations of their source choreography, making developers more productive, and preventing them from writing incompatible implementations of communications.

Choral is currently interoperable with Java and it is compatible with Java in three ways:

Papers

Giallorenzo, S., Montesi, F. and Peressotti, M. 2024. Choral: Object-oriented Choreographic Programming. ACM Trans. Program. Lang. Syst. 46, 1 (2024), 1:1–1:59. DOI:10.1145/3632398.

Choreographies are coordination plans for concurrent and distributed systems, which define the roles of the involved participants and how they are supposed to work together. In the paradigm of choreographic programming, choreographies are programs that can be compiled into executable implementations.

In this article, we present Choral, the first choreographic programming language based on mainstream abstractions. The key idea in Choral is a new notion of data type, which allows for expressing that data is distributed over different roles. We use this idea to reconstruct the paradigm of choreographic programming through object-oriented abstractions. Choreographies are classes, and instances of choreographies are objects with states and behaviours implemented collaboratively by roles.

Choral comes with a compiler that, given a choreography, generates an implementation for each of its roles. These implementations are libraries in pure Java, whose types are under the control of the Choral programmer. Developers can then modularly compose these libraries in their programs, to participate correctly in choreographies. Choral is the first incarnation of choreographic programming offering such modularity, which finally connects more than a decade of research on the paradigm to practical software development.

The integration of choreographic and object-oriented programming yields other powerful advantages, where the features of one paradigm benefit the other in ways that go beyond the sum of the parts. On the one hand, the high-level abstractions and static checks from the world of choreographies can be used to write concurrent and distributed object-oriented software more concisely and correctly. On the other hand, we obtain a much more expressive choreographic language from object-oriented abstractions than in previous work. This expressivity allows for writing more reusable and flexible choreographies. For example, object passing makes Choral the first higher-order choreographic programming language, whereby choreographies can be parameterised over other choreographies without any need for central coordination. We also extend method overloading to a new dimension: specialisation based on data location. Together with subtyping and generics, this allows Choral to elegantly support user-defined communication mechanisms and middleware.

@article{GMP24,
  author = {Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco},
  title = {Choral: Object-oriented Choreographic Programming},
  year = {2024},
  issue_date = {March 2024},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  journal = {ACM Trans. Program. Lang. Syst.},
  volume = {46},
  number = {1},
  pages = {1:1--1:59},
  issn = {0164-0925},
  url = {https://doi.org/10.1145/3632398},
  doi = {10.1145/3632398},
  keywords = {Communication, Higher-Kinded Types, Choreographies}
}
Plyukhin, D., Montesi, F. and Peressotti, M. 2024. Ozone: Fully Out-of-Order Choreographies. CoRR. abs/2401.17403, (2024). DOI:10.48550/arXiv.2401.17403.

Choreographic programming is a paradigm for writing distributed applications. It allows programmers to write a single program, called a choreography, that can be compiled to generate correct implementations of each process in the application. Although choreographies provide good static guarantees, they can exhibit high latency when messages or processes are delayed. This is because processes in a choreography typically execute in a fixed, deterministic order, and cannot adapt to the order that messages arrive at runtime. In non-choreographic code, programmers can address this problem by allowing processes to execute out of order – for instance by using futures or reactive programming. However, in choreographic code, out-of-order process execution can lead to serious and subtle bugs, called communication integrity violations (CIVs).

In this paper, we develop a model of choreographic programming for out-of-order processes that guarantees absence of CIVs and deadlocks. As an application of our approach, we also introduce an API for safe non-blocking communication via futures in the choreographic programming language Choral. The API allows processes to execute out of order, participate in multiple choreographies concurrently, and to handle unordered or dropped messages as in the UDP transport protocol. We provide an illustrative evaluation of our API, showing that out-of-order execution can reduce latency by overlapping communication with computation.

@article{abs-2401-17403,
  title = {Ozone: Fully Out-of-Order Choreographies},
  author = {Plyukhin, Dan and Montesi, Fabrizio and Peressotti, Marco},
  journal = {CoRR},
  volume = {abs/2401.17403},
  year = {2024},
  url = {https://arxiv.org/abs/2401.17403},
  doi = {10.48550/arXiv.2401.17403},
  archiveprefix = {arXiv},
  eprint = {2401.17403}
}
Giallorenzo, S., Montesi, F., Peressotti, M., Richter, D., Salvaneschi, G. and Weisenburger, P. 2021. Multiparty Languages: The Choreographic and Multitier Cases. 35th European Conference on Object-Oriented Programming (ECOOP 2021) (Dagstuhl, Germany, 2021), 22:1–22:27.

Choreographic languages aim to express multiparty communication protocols, by providing primitives that make interaction manifest. Multitier languages enable programming computation that spans across several tiers of a distributed system, by supporting primitives that allow computation to change the location of execution. Rooted into different theoretical underpinnings—respectively process calculi and lambda calculus—the two paradigms have been investigated independently by different research communities with little or no contact. As a result, the link between the two paradigms has remained hidden for long.

In this paper, we show that choreographic languages and multitier languages are surprisingly similar. We substantiate our claim by isolating the core abstractions that differentiate the two approaches and by providing algorithms that translate one into the other in a straightforward way. We believe that this work paves the way for joint research and cross-fertilisation among the two communities.

@inproceedings{GMPRSW21,
  author = {Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco and Richter, David and Salvaneschi, Guido and Weisenburger, Pascal},
  title = {{Multiparty Languages: The Choreographic and Multitier Cases}},
  booktitle = {35th European Conference on Object-Oriented Programming (ECOOP 2021)},
  pages = {22:1--22:27},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  isbn = {978-3-95977-190-0},
  issn = {1868-8969},
  year = {2021},
  volume = {194},
  editor = {M{\o}ller, Anders and Sridharan, Manu},
  publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address = {Dagstuhl, Germany},
  url = {https://drops.dagstuhl.de/opus/volltexte/2021/14065},
  urn = {urn:nbn:de:0030-drops-140658},
  doi = {10.4230/LIPIcs.ECOOP.2021.22}
}
Giallorenzo, S., Montesi, F. and Peressotti, M. 2020. Choral: Object-Oriented Choreographic Programming. CoRR. abs/22005.09520, (2020). DOI:10.48550/arXiv.2005.09520.

We present Choral, the first language for programming choreographies (multiparty protocols) that builds on top of mainstream programming abstractions: in Choral, choreographies are objects. Given a choreography that defines interactions among some roles (Alice, Bob, etc.), an implementation for each role in the choreography is automatically generated by a compiler. These implementations are libraries in pure Java, which developers can modularly compose in their own programs to participate correctly in choreographies.

@article{abs-2005-09520,
  author = {Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco},
  title = {Choral: Object-Oriented Choreographic Programming},
  journal = {CoRR},
  volume = {abs/22005.09520},
  year = {2020},
  url = {https://arxiv.org/abs/2005.09520},
  doi = {10.48550/arXiv.2005.09520},
  archiveprefix = {arXiv},
  eprint = {2005.09520}
}