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

<span class="mw-page-title-main">Kerberos (protocol)</span> Computer authentication protocol

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.

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 computer science, instruction selection is the stage of a compiler backend that transforms its middle-level intermediate representation (IR) into a low-level IR. In a typical compiler, instruction selection precedes both instruction scheduling and register allocation; hence its output IR has an infinite set of pseudo-registers and may still be – and typically is – subject to peephole optimization. Otherwise, it closely resembles the target machine code, bytecode, or assembly language.

A bigraph can be modelled as the superposition of a graph and a set of trees.

A fundamental problem in distributed computing and multi-agent systems is to achieve overall system reliability in the presence of a number of faulty processes. This often requires coordinating processes to reach consensus, or agree on some data value that is needed during computation. Example applications of consensus include agreeing on what transactions to commit to a database in which order, state machine replication, and atomic broadcasts. Real-world applications often requiring consensus include cloud computing, clock synchronization, PageRank, opinion formation, smart power grids, state estimation, control of UAVs, load balancing, blockchain, and others.

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, Meta Platforms, Microsoft, and Twitter to permit users to share information about their accounts with third-party applications or websites.

<span class="mw-page-title-main">Multi-factor authentication</span> Method of computer access control

Multi-factor authentication is an electronic authentication method in which a user is granted access to a website or application only after successfully presenting two or more pieces of evidence to an authentication mechanism. MFA protects personal data—which may include personal identification or financial assets—from being accessed by an unauthorized third party that may have been able to discover, for example, a single password.

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.

In authentication, risk-based authentication is a non-static authentication system which takes into account the profile of the agent requesting access to the system to determine the risk profile associated with that transaction. The risk profile is then used to determine the complexity of the challenge. Higher risk profiles leads to stronger challenges, whereas a static username/password may suffice for lower-risk profiles. Risk-based implementation allows the application to challenge the user for additional credentials only when the risk level is appropriate.

Machine authentication is often used in a risk based authentication set up. The machine authentication will run in the background and only ask the customer for additional authentication if the computer is not recognized. In a risk based authentication system, the institution decides if additional authentication is necessary. If the risk is deemed appropriate, enhanced authentication will be triggered, such as a one time password delivered via an out of band communication. Risk based authentication can also be used during the session to prompt for additional authentication when the customer performs a certain high risk transaction, such as a money transfer or an address change. Risk based authentication is very beneficial to the customer because additional steps are only required if something is out of the ordinary, such as the login attempt is from a new machine.

<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.

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

A social bot, also described as a social AI or social algorithm, is a software agent that communicates autonomously on social media. The messages it distributes can be simple and operate in groups and various configurations with partial human control (hybrid) via algorithm. Social bots can also use artificial intelligence and machine learning to express messages in more natural human dialogue.

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.

Differentiable programming is a programming paradigm in which a numeric computer program can be differentiated throughout via automatic differentiation. This allows for gradient-based optimization of parameters in the program, often via gradient descent, as well as other learning approaches that are based on higher order derivative information. Differentiable programming has found use in a wide variety of areas, particularly scientific computing and machine learning. One of the early proposals to adopt such a framework in a systematic fashion to improve upon learning algorithms was made by the Advanced Concepts Team at the European Space Agency in early 2016.

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.

In economics, a budget-additive valuation is a kind of a utility function. It corresponds to a person that, when given a set of items, evaluates them in the following way:

In type theory, session types are used to ensure correctness in concurrent programs. They guarantee that messages sent and received between concurrent programs are in the expected order and of the expected type. Session type systems have been adapted for both channel and actor systems.

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. ↑ 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.
  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. arXiv: 1510.03271 . doi:10.1016/j.tcs.2019.07.005. S2CID   199122777.
  19. ↑ 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.
  20. ↑ 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.
  21. ↑ Cruz-Filipe, Luís; Montesi, Fabrizio; Peressotti, Marco (2021). Cerone, Antonio; Ölveczky, Peter Csaba (eds.). Certifying Choreography Compilation. Lecture Notes in Computer Science. Vol. 12819. Cham: Springer International Publishing. 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.{{cite book}}: |work= ignored (help)
  22. ↑ Shen, Gan; Kashiwa, Shun; Kuper, Lindsey (2023-08-31). "HasChor: Functional Choreographic Programming for All (Functional Pearl)". HasChor. 7 (ICFP): 207:541–207:565. arXiv: 2303.00924 . doi: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). 237. Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum für Informatik: 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.