Choreographic programming

Last updated

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

Contents

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:

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 choreography
Client
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


See also

Related Research Articles

Kerberos is a computer-network authentication protocol that works on the basis of tickets to allow nodes communicating over a non-secure network to prove their identity to one another in a secure manner. Its designers aimed it primarily at a client–server model, and it provides mutual authentication—both the user and the server verify each other's identity. Kerberos protocol messages are protected against eavesdropping and replay attacks.

In cryptography, security (engineering) protocol notation, also known as protocol narrations and Alice & Bob notation, is a way of expressing a protocol of correspondence between entities of a dynamic system, such as a computer network. In the context of a formal model, it allows reasoning about the properties of such a system.

A replay attack is a form of network attack in which valid data transmission is maliciously or fraudulently repeated or delayed. This is carried out either by the originator or by an adversary who intercepts the data and re-transmits it, possibly as part of a spoofing attack by IP packet substitution. This is one of the lower-tier versions of a man-in-the-middle attack. Replay attacks are usually passive in nature.

In computing, an effect system is a formal system that describes the computational effects of computer programs, such as side effects. An effect system can be used to provide a compile-time check of the possible effects of the program.

In cryptography, a password-authenticated key agreement method is an interactive method for two or more parties to establish cryptographic keys based on one or more party's knowledge of a password.

In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involving real numbers, integers, and/or various data structures such as lists, arrays, bit vectors, and strings. The name is derived from the fact that these expressions are interpreted within ("modulo") a certain formal theory in first-order logic with equality. SMT solvers are tools that aim to solve the SMT problem for a practical subset of inputs. SMT solvers such as Z3 and cvc5 have been used as a building block for a wide range of applications across computer science, including in automated theorem proving, program analysis, program verification, and software testing.

OAuth is an open standard for access delegation, commonly used as a way for internet users to grant websites or applications access to their information on other websites but without giving them the passwords. This mechanism is used by companies such as Amazon, Google, Facebook, Microsoft, and Twitter to permit users to share information about their accounts with third-party applications or websites.

RTMPDump is a free software project dedicated to develop a toolkit for RTMP streams. The package includes three programs, rtmpdump, rtmpsrv and rtmpsuck.

Service choreography in business computing is a form of service composition in which the interaction protocol between several partner services is defined from a global perspective. The idea underlying the notion of service choreography can be summarised as follows:

"Dancers dance following a global scenario without a single point of control"

SMTP Authentication, often abbreviated SMTP AUTH, is an extension of the Simple Mail Transfer Protocol (SMTP) whereby a client may log in using any authentication mechanism supported by the server. It is mainly used by submission servers, where authentication is mandatory.

<span class="mw-page-title-main">Jolie (programming language)</span>

Jolie is an open-source programming language for developing distributed applications based on microservices. In the programming paradigm proposed with Jolie, each program is a service that can communicate with other programs by sending and receiving messages over a network. Jolie supports an abstraction layer that allows services to communicate using different mediums, ranging from TCP/IP sockets to local in-memory communications between processes.

Gradual typing is a type system in which some variables and expressions may be given types and the correctness of the typing is checked at compile time and some expressions may be left untyped and eventual type errors are reported at runtime. Gradual typing allows software developers to choose either type paradigm as appropriate, from within a single language. In many cases gradual typing is added to an existing dynamic language, creating a derived language allowing but not requiring static typing to be used. In some cases a language uses gradual typing from the start.

Web API security entails authenticating programs or users who are invoking a web API.

<span class="mw-page-title-main">Tamarin Prover</span>

Tamarin Prover is a computer software program for formal verification of cryptographic protocols. It has been used to verify Transport Layer Security 1.3, ISO/IEC 9798, DNP3 Secure Authentication v5, and WireGuard.

Executable choreography represents a decentralized form of service composition, involving the cooperation of several individual entities. It is an improved form of service choreography. Executable choreographies can be intuitively seen as arbitrary complex workflows that get executed in systems belonging to multiple organisations or authorities.

IndieAuth is an open standard decentralized authentication protocol that uses OAuth 2.0 and enables services to verify the identity of a user represented by a URL, as well as to obtain an access token, that can be used to access resources under the control of the user.

Runtime predictive analysis is a runtime verification technique in computer science for detecting property violations in program executions inferred from an observed execution. An important class of predictive analysis methods has been developed for detecting concurrency errors in concurrent programs, where a runtime monitor is used to predict errors which did not happen in the observed run, but can happen in an alternative execution of the same program. The predictive capability comes from the fact that the analysis is performed on an abstract model extracted online from the observed execution, which admits a class of executions beyond the observed one.

Multitier programming is a programming paradigm for distributed software, which typically follows a multitier architecture, physically separating different functional aspects of the software into different tiers. Multitier programming allows functionalities that span multiple of such tiers to be developed in a single compilation unit using a single programming language. Without multitier programming, tiers are developed using different languages, e.g., JavaScript for the Web client, PHP for the Web server and SQL for the database. Multitier programming is often integrated into general-purpose languages by extending them with support for distribution.

The International Symposium on Experimental Algorithms (SEA), previously known as Workshop on Experimental Algorithms (WEA), is a computer science conference in the area of algorithm engineering.

In computer science and mathematical logic, Cooperating Validity Checker (CVC) is a family of satisfiability modulo theories (SMT) solvers. The latest major versions of CVC are CVC4 and CVC5 ; earlier versions include CVC, CVC Lite, and CVC3. Both CVC4 and cvc5 support the SMT-LIB and TPTP input formats for solving SMT problems, and the SyGuS-IF format for program synthesis. Both CVC4 and cvc5 can output proofs that can be independently checked in the LFSC format, cvc5 additionally supports the Alethe and Lean 4 formats. cvc5 has bindings for C++, Python, and Java.

References

  1. 1 2 3 4 5 Montesi, Fabrizio (2023). Introduction to Choreographies. Cambridge University Press. doi:10.1017/9781108981491. ISBN   978-1-108-83376-9. S2CID   102335067.
  2. 1 2 3 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 (2016). "Behavioral Types in Programming Languages". Foundations and Trends in Programming Languages. 3 (2–3): 95–230. doi:10.1561/2500000031. hdl: 10044/1/44282 .
  3. 1 2 3 4 5 6 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). Vol. 194. pp. 22:1–22:27. doi:10.4230/LIPIcs.ECOOP.2021.22. ISBN   9783959771900. (ECOOP 2021 Distinguished Paper)
  4. ↑ Choral programming language
  5. 1 2 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. S2CID   15627190.
  6. 1 2 3 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. S2CID   5555662.
  7. ↑ Montesi, Fabrizio (2013). Choreographic Programming (PDF) (PhD). IT University of Copenhagen. ISBN   978-87-7949-299-8. (EAPLS Best PhD Dissertation Award)
  8. 1 2 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. arXiv: 2111.03484 . doi: 10.1145/3498684 . S2CID   243833095. (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.
  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 . S2CID   15737118.
  11. ↑ Lluch Lafuente, Alberto; Nielson, Flemming; Nielson, Hanne Riis (2015). "Discretionary Information Flow Control for Interaction-Oriented Specifications". Logic, Rewriting, and Concurrency (PDF). Lecture Notes in Computer Science. Vol. 9200. pp. 427–450. doi:10.1007/978-3-319-23165-5_20. ISBN   978-3-319-23164-8. S2CID   32617923.
  12. ↑ Cruz-Filipe, Luís; Montesi, Fabrizio (2016). "Choreographies in Practice". Formal Techniques for Distributed Objects, Components, and Systems. Lecture Notes in Computer Science. Vol. 9688. pp. 114–123. arXiv: 1602.08863 . doi:10.1007/978-3-319-39570-8_8. ISBN   978-3-319-39569-2. S2CID   18067252.
  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. S2CID   39112346.
  14. ↑ López, Hugo A.; Nielson, Flemming; Nielson, Hanne Riis (2016). "Enforcing Availability in Failure-Aware Communicating Systems" (PDF). Formal Techniques for Distributed Objects, Components, and Systems. Lecture Notes in Computer Science. Vol. 9688. pp. 195–211. doi:10.1007/978-3-319-39570-8_13. ISBN   978-3-319-39569-2. S2CID   12872876.
  15. ↑ Giallorenzo, Saverio; Lanese, Ivan; Russo, Daniel (2018). "ChIP: A Choreographic Integration Process". On the Move to Meaningful Internet Systems. OTM 2018 Conferences (PDF). Lecture Notes in Computer Science. Vol. 11230. pp. 22–40. doi:10.1007/978-3-030-02671-4_2. ISBN   978-3-030-02670-7. S2CID   53015580.
  16. ↑ Cruz-Filipe, Luís; Montesi, Fabrizio (2020). "A core model for choreographic programming". Theoretical Computer Science. 802: 38–66. arXiv: 1510.03271 . doi:10.1016/j.tcs.2019.07.005. S2CID   199122777.
  17. ↑ Cohen, Liron; Kaliszyk, Cezary (2021). Formalising a Turing-Complete Choreographic Language in Coq. Leibniz International Proceedings in Informatics (LIPIcs). Vol. 193. pp. 15:1–15:18. doi:10.4230/LIPIcs.ITP.2021.15. ISBN   9783959771887. S2CID   231802115.
  18. ↑ Cruz-Filipe, Luís; Montesi, Fabrizio; Peressotti, Marco (2023-05-27). "A Formal Theory of Choreographic Programming". Journal of Automated Reasoning. 67 (2): 21. arXiv: 2209.01886 . doi: 10.1007/s10817-023-09665-3 . ISSN   1573-0670. S2CID   252090305.
  19. ↑ Cruz-Filipe, Luís; Montesi, Fabrizio; Peressotti, Marco (2021), Cerone, Antonio; Ölveczky, Peter Csaba (eds.), "Certifying Choreography Compilation", Theoretical Aspects of Computing – ICTAC 2021, Lecture Notes in Computer Science, Cham: Springer International Publishing, vol. 12819, pp. 115–133, arXiv: 2102.10698 , doi:10.1007/978-3-030-85315-0_8, ISBN   978-3-030-85314-3, S2CID   231985665 , retrieved 2022-03-07
  20. ↑ 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. S2CID   251322644.
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.