Choreographic programming explained

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

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 exampleAlice.expr -> Bob.xreads "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:

The choreography is:Client.(credentials, serviceID) -> CAS.authRequestif CAS.check(authRequest) then CAS.token = genToken(authRequest) CAS.Success(token) -> Client.result CAS.Success(token) -> Service.resultelse 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] [4] or standalone distributed programs.

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

Endpoint projection returns a program for each role described in the source choreography. 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.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.[5] [6] [7] 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] [8]

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

Languages

See also

External links

Notes and References

  1. Book: Montesi . Fabrizio . Introduction to Choreographies . 2023 . Cambridge University Press . 10.1017/9781108981491 . 978-1-108-83376-9 . 102335067 .
  2. Behavioral Types in Programming Languages. 10.1561/2500000031. 2016. Yoshida. Nobuko. Vasconcelos. Vasco T.. Padovani. Luca. Bono. Nicholas Ng. Neykova. Rumyana. Montesi. Fabrizio. Mascardi. Viviana. Martins. Francisco. Johnsen. Einar Broch. Hu. Raymond. Giachino. Elena. Gesbert. Nils. Gay. Simon J.. Deniélou. Pierre-Malo. Castagna. Giuseppe. Campos. Joana. Bravetti. Mario. Bono. Viviana. Ancona. Davide. Foundations and Trends in Programming Languages. 3. 2–3. 95–230. 10044/1/44282 . free.
  3. Book: 10.4230/LIPIcs.ECOOP.2021.22. 2021. Giallorenzo. Saverio. Montesi. Fabrizio. Peressotti. Marco. Richter. David. Salvaneschi. Guido. Weisenburger. Pascal. Multiparty Languages: The Choreographic and Multitier Cases (Pearl). Leibniz International Proceedings in Informatics (LIPIcs). 194. 22:1–22:27. free . 9783959771900. (ECOOP 2021 Distinguished Paper)
  4. https://www.choral-lang.org/ Choral programming language
  5. PhD . Montesi . Fabrizio . 2013 . Choreographic Programming . IT University of Copenhagen . 978-87-7949-299-8. (EAPLS Best PhD Dissertation Award)
  6. Hirsch . Andrew K. . Garg . Deepak . Pirouette: higher-order typed functional choreographies . Proceedings of the ACM on Programming Languages . 16 January 2022 . 6 . POPL . 1–27 . 10.1145/3498684. 243833095 . free . 2111.03484 . (POPL 2022 Distinguished Paper)
  7. Web site: Fabrizio Montesi wins the EAPLS Best PhD Dissertation Award 2014 . Arend Rensink . 2015-08-30 . European Association for Programming Languages and Systems.
  8. 10.1145/2220365.2220367. Structured Communication-Centered Programming for Web Services. 2012. Carbone. Marco. Honda. Kohei. Yoshida. Nobuko. ACM Transactions on Programming Languages and Systems. 34. 2. 1–78. 15737118. free.
  9. Book: https://doi.org/10.1007/978-3-319-23165-5_20. 10.1007/978-3-319-23165-5_20. Discretionary Information Flow Control for Interaction-Oriented Specifications. Logic, Rewriting, and Concurrency. Lecture Notes in Computer Science. 2015. Lluch Lafuente. Alberto. Nielson. Flemming. Nielson. Hanne Riis. Hanne Riis Nielson. 9200. 427–450. 978-3-319-23164-8. 32617923 .
  10. Book: https://doi.org/10.1007/978-3-319-39570-8_8. 10.1007/978-3-319-39570-8_8. Choreographies in Practice. Formal Techniques for Distributed Objects, Components, and Systems. Lecture Notes in Computer Science. 2016. Cruz-Filipe. Luís. Montesi. Fabrizio. 9688. 114–123. 1602.08863. 978-3-319-39569-2. 18067252.
  11. Book: https://doi.org/10.1145/3019612.3019656. 10.1145/3019612.3019656. Choreographing cyber-physical distributed control systems for the energy sector. Proceedings of the Symposium on Applied Computing. 2017. López. Hugo A.. Heussen. Kai. 437–443. 9781450344869. 39112346.
  12. Book: https://backend.orbit.dtu.dk/ws/files/123934557/main.pdf. 10.1007/978-3-319-39570-8_13. Enforcing Availability in Failure-Aware Communicating Systems. Formal Techniques for Distributed Objects, Components, and Systems. Lecture Notes in Computer Science. 2016. López. Hugo A.. Nielson. Flemming. Nielson. Hanne Riis. Hanne Riis Nielson. 9688. 195–211. 978-3-319-39569-2. 12872876 .
  13. Dynamic Choreographies: Theory and Implementation. 10.23638/LMCS-13(2:1)2017. 2017. Preda. Mila Dalla. Gabbrielli. Maurizio. Giallorenzo. Saverio. Lanese. Ivan. Mauro. Jacopo. Logical Methods in Computer Science . 13. 2. 5555662.
  14. Book: https://doi.org/10.1007/978-3-030-02671-4_2. 10.1007/978-3-030-02671-4_2. ChIP: A Choreographic Integration Process. On the Move to Meaningful Internet Systems. OTM 2018 Conferences. Lecture Notes in Computer Science. 2018. Giallorenzo. Saverio. Lanese. Ivan. Russo. Daniel. 11230. 22–40. 978-3-030-02670-7. 53015580 .
  15. Book: https://doi.org/10.1145/2429069.2429101. 10.1145/2429069.2429101. Deadlock-freedom-by-design. Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '13. 2013. Carbone. Marco. Montesi. Fabrizio. 263. 9781450318327. 15627190.
  16. A core model for choreographic programming. 10.1016/j.tcs.2019.07.005. 2020. Cruz-Filipe. Luís. Montesi. Fabrizio. Theoretical Computer Science. 802. 38–66. 199122777. 1510.03271.
  17. Book: 10.4230/LIPIcs.ITP.2021.15. 9783959771887. Formalising a Turing-Complete Choreographic Language in Coq. Leibniz International Proceedings in Informatics (LIPIcs). 2021. 193. 15:1–15:18. Cohen. Liron. Kaliszyk. Cezary. free . 231802115.
  18. Cruz-Filipe . Luís . Montesi . Fabrizio . Peressotti . Marco . 2023-05-27 . A Formal Theory of Choreographic Programming . Journal of Automated Reasoning . en . 67 . 2 . 21 . 10.1007/s10817-023-09665-3 . 252090305 . 1573-0670. free . 2209.01886 .
  19. Shen . Gan . Kashiwa . Shun . Kuper . Lindsey . 2023-08-31 . HasChor: Functional Choreographic Programming for All (Functional Pearl) . HasChor . 7 . ICFP . 207:541–207:565 . 10.1145/3607849. 2303.00924 .
  20. Pohjola . Johannes Åman . Gómez-Londoño . Alejandro . Shaker . James . Norrish . Michael . 2022 . Andronick . June . de Moura . Leonardo . 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 . 10.4230/LIPIcs.ITP.2022.27 . free . 978-3-95977-252-5. 251322644 .

This article is licensed under the GNU Free Documentation License. It uses material from the Wikipedia article "Choreographic programming".

Except where otherwise indicated, Everything.Explained.Today is © Copyright 2009-2024, A B Cryer, All Rights Reserved. Cookie policy.