Choreographic programming

Short description: Programming paradigm

In computer science, choreographic programming is a programming paradigm for distributed systems, where programs are written as compositions of interactions among multiple concurrent participants.[1][2][3]

Deadlock is a common error that can occur in distributed systems. Choreographic programming ensures that deadlock cannot occur in the scope of the choreography by ensuring that every time a message is sent from one party, there is a corresponding receive on the other end.

## Contents

* 1 Overview
* 1.1 Choreographies
* 1.2 Endpoint Projection
* 2 Development
* 3 Languages
* 4 See also
* 5 References
* 6 External links

## Overview

### Choreographies

In choreographic programming, developers use a choreographic programming language to define the intended communication behaviour of concurrent participants. Programs in this paradigm are called choreographies.[1] Choreographic languages are inspired by security protocol notation (also known as "Alice and Bob" notation). The key to these languages is the communication primitive, for example

Alice.expr -> Bob.x

reads "`Alice` communicates the result of evaluating the expression `expr` to `Bob`, which stores it in its local variable `x`".[3] Alice, Bob, etc. are typically called roles or processes.[2]

The example below shows a choreography for a simplified single sign-on (SSO) protocol based on a Central Authentication Service (CAS) that involves three roles:

* `Client`, which wishes to obtain an access token from `CAS` to interact with `Service`.
* `Service`, which needs to know from `CAS` if the `Client` should be given access.
* `CAS`, which is the Central Authentication Service responsible for checking the `Client`'s credentials.

The choreography is:

Client.(credentials, serviceID) -> CAS.authRequest
if CAS.check(authRequest) then
CAS.token = genToken(authRequest)
CAS.Success(token) -> Client.result
CAS.Success(token) -> Service.result
else
CAS.Failure -> Client.result
CAS.Failure -> Service.result

The choreography starts in Line 1, where `Client` communicates a pair consisting of some credentials and the identifier of the service it wishes to access to `CAS`. `CAS` stores this pair in its local variable `authRequest` (for authentication request). In Line 2, the `CAS` checks if the request is valid for obtaining an authentication token. If so, it generates a token and communicates a `Success` message containing the token to both `Client` and `Service` (Lines 3–5). Otherwise, the `CAS` informs `Client` and `Service` that authentication failed, by sending a `Failure` message (Lines 7–8). We refer to this choreography as the "SSO choreography" in the remainder.

### Endpoint Projection

A key feature of choreographic programming is the capability of compiling choreographies to distributed implementations. These implementations can be libraries for software that needs to participate in a computer network by following a protocol,[1][3][4] or standalone distributed programs.[5][6]

The translation of a choreography into distributed programs is called endpoint projection (EPP for short).[2][3]

Endpoint projection returns a program for each role described in the source choreography.[3] For example, given the choreography above, endpoint projection would return three programs: one for `Client`, one for `Service`, and one for `CAS`. They are shown below in pseudocode form, where `send` and `recv` are primitives for sending and receiving messages to/from other roles.

Endpoint Projection (EPP) of the SSO choreographyClient|

send (credentials, serviceID) to CAS
recv result from CAS

|

Service|

recv result from CAS

CAS|

recv authRequest from Client
if check(authRequest) then
token = genToken(authRequest)
send Success(token) to Client
send Success(token) to Service
else
send Failure to Client
send Failure to Service

For each role, its code contains the actions that the role should execute to implement the choreography correctly together with the others.

## Development

The paradigm of choreographic programming originates from its titular PhD thesis.[7][8][9] The inspiration for the syntax of choreographic programming languages can be traced back to security protocol notation, also known as "Alice and Bob" notation.[1] Choreographic programming has also been heavily influenced by standards for service choreography and interaction diagrams, as well as developments of the theory of process calculi.[1][3][10]

Choreographic programming is an active area of research. The paradigm has been used in the study of information flow,[11] parallel computing,[12] cyber-physical systems,[13][14] runtime adaptation,[6] and system integration.[15]

## Languages

* AIOCJ (website).[6] A choreographic programming language for adaptable systems that produces code in Jolie.
* Chor.[5] A session-typed choreographic programming language that compiled to microservices in Jolie. In the meantime superseded by Choral.
* Choral (website).[16][17] An object-oriented choreographic programming language that compiles to libraries in Java. Choral is the first choreographic programming language with decentralised data structures and higher-order parameters.
* Chorex (website). An Elixir library providing an embedded choreographic programming language through Elixir's macro system.
* ChoRus (website). Library-level choreographic programming in Rust.
* Core Choreographies.[18] A core theoretical model for choreographic programming. A mechanised implementation is available in Rocq.[19][20][21]
* HasChor (website).[22] A library for choreographic programming in Haskell.
* Kalas.[23] A choreographic programming language with a verified compiler to CakeML.
* Pirouette.[8] A mechanised choreographic programming language theory with higher-order procedures.
* Klor (website). Library-level choreographic programming in Clojure.
* Tempo (website). A practical choreographic programming language that compiles to library source code for multiple target languages.

## See also

* Security protocol notation
* Sequence diagram
* Service choreography
* Structured concurrency
* Multitier programming

## References

1. ↑ 1.0 1.1 1.2 1.3 1.4 Montesi, Fabrizio (2023). Introduction to Choreographies. Cambridge University Press. doi:10.1017/9781108981491. ISBN 978-1-108-83376-9. https://doi.org/10.1017/9781108981491.
2. ↑ 2.0 2.1 2.2 Yoshida, Nobuko; Vasconcelos, Vasco T.; Padovani, Luca; Bono, Nicholas Ng; Neykova, Rumyana; Montesi, Fabrizio; Mascardi, Viviana; Martins, Francisco et al. (2016). "Behavioral Types in Programming Languages". Foundations and Trends in Programming Languages 3 (2–3): 95–230. doi:10.1561/2500000031. https://doi.org/10.1561/2500000031.
3. ↑ 3.0 3.1 3.2 3.3 3.4 3.5 Giallorenzo, Saverio; Montesi, Fabrizio; Peressotti, Marco; Richter, David; Salvaneschi, Guido; Weisenburger, Pascal (2021). Multiparty Languages: The Choreographic and Multitier Cases (Pearl). Leibniz International Proceedings in Informatics (LIPIcs). 194. pp. 22:1–22:27. doi:10.4230/LIPIcs.ECOOP.2021.22. ISBN 9783959771900. (ECOOP 2021 Distinguished Paper)
4. ↑ Choral programming language
5. ↑ 5.0 5.1 Carbone, Marco; Montesi, Fabrizio (2013). "Deadlock-freedom-by-design". Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '13. p. 263. doi:10.1145/2429069.2429101. ISBN 9781450318327. https://doi.org/10.1145/2429069.2429101.
6. ↑ 6.0 6.1 6.2 Preda, Mila Dalla; Gabbrielli, Maurizio; Giallorenzo, Saverio; Lanese, Ivan; Mauro, Jacopo (2017). "Dynamic Choreographies: Theory and Implementation". Logical Methods in Computer Science 13 (2). doi:10.23638/LMCS-13(2:1)2017. https://doi.org/10.23638/LMCS-13(2:1)2017.
7. ↑ Montesi, Fabrizio (2013). Choreographic Programming (PDF) (PhD). IT University of Copenhagen. ISBN 978-87-7949-299-8. (EAPLS Best PhD Dissertation Award)
8. ↑ 8.0 8.1 Hirsch, Andrew K.; Garg, Deepak (16 January 2022). "Pirouette: higher-order typed functional choreographies". Proceedings of the ACM on Programming Languages 6 (POPL): 1–27. doi:10.1145/3498684. (POPL 2022 Distinguished Paper)
9. ↑ Arend Rensink (2015-08-30). "Fabrizio Montesi wins the EAPLS Best PhD Dissertation Award 2014". European Association for Programming Languages and Systems. https://eapls.org/items/1855/.
10. ↑ Carbone, Marco; Honda, Kohei; Yoshida, Nobuko (2012). "Structured Communication-Centered Programming for Web Services". ACM Transactions on Programming Languages and Systems 34 (2): 1–78. doi:10.1145/2220365.2220367.
11. ↑ Lluch Lafuente, Alberto; Nielson, Flemming; Nielson, Hanne Riis (2015). "Discretionary Information Flow Control for Interaction-Oriented Specifications". Logic, Rewriting, and Concurrency. Lecture Notes in Computer Science. 9200. pp. 427–450. doi:10.1007/978-3-319-23165-5_20. ISBN 978-3-319-23164-8. https://doi.org/10.1007/978-3-319-23165-5_20.
12. ↑ Cruz-Filipe, Luís; Montesi, Fabrizio (2016). "Choreographies in Practice". Formal Techniques for Distributed Objects, Components, and Systems. Lecture Notes in Computer Science. 9688. pp. 114–123. doi:10.1007/978-3-319-39570-8_8. ISBN 978-3-319-39569-2. https://doi.org/10.1007/978-3-319-39570-8_8.
13. ↑ López, Hugo A.; Heussen, Kai (2017). "Choreographing cyber-physical distributed control systems for the energy sector". Proceedings of the Symposium on Applied Computing. pp. 437–443. doi:10.1145/3019612.3019656. ISBN 9781450344869. https://doi.org/10.1145/3019612.3019656.
14. ↑ López, Hugo A.; Nielson, Flemming; Nielson, Hanne Riis (2016). "Enforcing Availability in Failure-Aware Communicating Systems". Formal Techniques for Distributed Objects, Components, and Systems. Lecture Notes in Computer Science. 9688. pp. 195–211. doi:10.1007/978-3-319-39570-8_13. ISBN 978-3-319-39569-2. https://inria.hal.science/hal-01432918.
15. ↑ Giallorenzo, Saverio; Lanese, Ivan; Russo, Daniel (2018). "ChIP: A Choreographic Integration Process". On the Move to Meaningful Internet Systems. OTM 2018 Conferences. Lecture Notes in Computer Science. 11230. pp. 22–40. doi:10.1007/978-3-030-02671-4_2. ISBN 978-3-030-02670-7. https://doi.org/10.1007/978-3-030-02671-4_2.
16. ↑ Giallorenzo, Saverio; Montesi, Fabrizio; Peressotti, Marco (2024-01-16). "Choral: Object-oriented Choreographic Programming". ACM Trans. Program. Lang. Syst. 46 (1): 1:1–1:59. doi:10.1145/3632398. ISSN 0164-0925. https://dl.acm.org/doi/10.1145/3632398.
17. ↑ Giallorenzo, Saverio; Montesi, Fabrizio; Peressotti, Marco (2023-10-19). "Choral: Object-Oriented Choreographic Programming". arXiv:2005.09520 [cs.PL].
18. ↑ Cruz-Filipe, Luís; Montesi, Fabrizio (2020). "A core model for choreographic programming". Theoretical Computer Science 802: 38–66. doi:10.1016/j.tcs.2019.07.005. https://doi.org/10.1016/j.tcs.2019.07.005.
19. ↑ Cohen, Liron; Kaliszyk, Cezary (2021). Formalising a Turing-Complete Choreographic Language in Coq. Leibniz International Proceedings in Informatics (LIPIcs). 193. pp. 15:1–15:18. doi:10.4230/LIPIcs.ITP.2021.15. ISBN 9783959771887.
20. ↑ Cruz-Filipe, Luís; Montesi, Fabrizio; Peressotti, Marco (2023-05-27). "A Formal Theory of Choreographic Programming" (in en). Journal of Automated Reasoning 67 (2): 21. doi:10.1007/s10817-023-09665-3. ISSN 1573-0670.
21. ↑ Cruz-Filipe, Luís; Montesi, Fabrizio; Peressotti, Marco (2021). Cerone, Antonio; Ölveczky, Peter Csaba. eds (in en). Certifying Choreography Compilation. Lecture Notes in Computer Science. 12819. Cham: Springer International Publishing. pp. 115–133. doi:10.1007/978-3-030-85315-0_8. ISBN 978-3-030-85314-3. https://link.springer.com/10.1007/978-3-030-85315-0_8. Retrieved 2022-03-07.
22. ↑ Shen, Gan; Kashiwa, Shun; Kuper, Lindsey (2023-08-31). "HasChor: Functional Choreographic Programming for All (Functional Pearl)". Proceedings of the ACM on Programming Languages 7: 541–565. doi:10.1145/3607849. https://doi.org/10.1145/3607849.
23. ↑ Pohjola, Johannes Åman; Gómez-Londoño, Alejandro; Shaker, James; Norrish, Michael (2022). Andronick, June; de Moura, Leonardo. eds. "Kalas: A Verified, End-To-End Compiler for a Choreographic Language". 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs) (Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum für Informatik) 237: 27:1–27:18. doi:10.4230/LIPIcs.ITP.2022.27. ISBN 978-3-95977-252-5. https://drops.dagstuhl.de/opus/volltexte/2022/16736.

## External links

* www.choral-lang.org

Template:Programming paradigms navbox

0.00

(0 votes)

Original source: https://en.wikipedia.org/wiki/Choreographic programming. Read more

|

Retrieved from "https://handwiki.org/wiki/index.php?title=Choreographic_programming&oldid=4226402"