Follow with Edit this page on Go back to the Bliki index

Choreographic Programming

By Fabrizio Montesi. Created on 2023-05-15. Last updated on 2024-11-19.
See also: Introduction to Choreographies and Choreographic Programming (Wikipedia).

Table of Contents (click to show)

Choreographic Programming is a programming paradigm where programs are choreographies [Montesi 2013]. These programs are written in choreographic programming languages, which feature high-level abstractions for defining the interactions and computations that independent processes engage in. A choreographic programming language is therefore a special case of a choreographic language. A program given in a choreographic programming language is called choreographic program, or simply choreography when it is clear from the context.

Alice.modPow(g, a, p) -> Bob.x;
Bob.modPow(g, b, p) -> Alice.y;

A snippet of the Diffie-Hellman protocol for key exchange, given in the language of Recursive Choreographies. The two archetypal processes Alice and Bob exchange data to establish a symmetric encryption key over a public channel (Wikipedia has a nice explanation of its parameters and cryptographic principles). The protocol specifies both communication and computation, making it an ideal candidate for being expressed in choreographic programming.

Endpoint Projection (EPP)

Choreographic programming languages are typically accompanied by a compiler, which translates choreographies into executable code for concurrent and distributed systems [Montesi 2023]. This code can form standalone applications, libraries, software connectors, etc. Libraries compiled from choreographies can be used in the modular development of distributed applications [Giallorenzo et al. 2020]. The theory of endpoint projection (EPP for short) usually plays an important role in the development of choreography compilers, in addition to the details of the target executable language.

Code for Alice:

send modPow(g, a, p) to Bob;
recv y from Bob;

Code for Bob:

recv x from Alice;
send modPow(g, b, p) to Alice;

Implementations of Alice and Bob compiled from the previous choreography, given in pseudocode.

In general a choreography might involve many participants, so EPP must be able to distribute code onto many target programs.

A choreography might define the collective behaviour of many processes. Compilation then returns an executable program for each process.

Ideally, EPP should not produce executable code that requires central control (unless this is specified explicitly by the source choreography): choreographies are intended to be decentralised. This introduces an interesting challenge known as knowledge of choice, which deals with ensuring that processes agrees on the alternative behaviours selected during the execution of the choreography.

Theories of EPP are also usually accompanied by proofs that the compiled code is deadlock-free. These proofs leverage the fact that source choreographies do not allow for pairing send and receive actions incorrectly (possibly under the assumption of some well-formedness or well-typedness conditions) [Montesi 2023]. The technique became popular under the slogan of 'deadlock-freedom by design' [Carbone and Montesi 2013].

Development

The term choreographic programming was coined in the titular PhD thesis [Montesi 2013], which proposed the approach as a programming paradigm. The paradigm builds on and extends a series of previous theoretical results on the design of choreographic languages and endpoint projection (e.g., message sequence charts, choreographies for web services, multiparty session types). For historical remarks and an introduction to theory of choreographies and their compilation, see Introduction to Choreographies [Montesi 2023].

Implementations

Mechanisations

There are several mechanisations of choreographic programming in theorem provers.

References

Carbone, M., Montesi, F. [2013], 'Deadlock-freedom-by-design: multiparty asynchronous global programming', POPL 2013 263-274. https://doi.org/10.1145/2429069.2429101

Cruz-Filipe, L., Lugovic, L., Montesi, F. [2023], 'Certified Compilation of Choreographies with hacc', Proc. FORTE, to appear. arXiv: https://doi.org/10.48550/arXiv.2303.03972

Cruz-Filipe, L., Montesi, F., Peressotti, M. [2023], 'A Formal Theory of Choreographic Programming', J. Autom. Reason. 67(2): 21. https://doi.org/10.1007/s10817-023-09665-3

Dalla Preda, M., Gabbrielli, M., Giallorenzo, S., Lanese, I., Mauro, J. [2017], 'Dynamic Choreographies: Theory And Implementation', Log. Methods Comput. Sci. 13(2). https://doi.org/10.23638/LMCS-13(2:1)2017

Giallorenzo, S., Montesi, F., Peressotti, M. [2024], 'Choral: Object-oriented Choreographic Programming', ACM Trans. Program. Lang. Syst. 46(1): 1:1-1:59. https://doi.org/10.1145/3632398

Hirsch, A. K., Garg, D. [2022], 'Pirouette: higher-order typed functional choreographies', Proc. ACM Program. Lang. 6(POPL): 1-27. https://doi.org/10.1145/3498684

Montesi, F. [2013], 'Choreographic Programming', PhD Thesis, IT University of Copenhagen. https://www.fabriziomontesi.com/files/choreographic-programming.pdf

Montesi, F. [2023], 'Introduction to Choreographies', Cambridge University Press. https://doi.org/10.1017/9781108981491

Pohjola, J. Å., Gómez-Londoño, A., Shaker, J., Norrish, M. [2022], 'Kalas: A Verified, End-To-End Compiler for a Choreographic Language', Proc. ITP 2022: 27:1-27:18. https://doi.org/10.4230/LIPIcs.ITP.2022.27

Shen, G., Kashiwa, S., Kuper, L. [2023], 'HasChor: Functional Choreographic Programming for All (Functional Pearl)', Proc. ACM Program. Lang. (ICFP), to appear. arXiv: https://doi.org/10.48550/arXiv.2303.00924