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 programming language theory, semantics is the rigorous mathematical study of the meaning of programming languages. Semantics assigns computational meaning to valid strings in a programming language syntax. It is closely related to, and often crosses over with, the semantics of mathematical proofs.

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.

Self-service password reset (SSPR) is defined as any process or technology that allows users who have either forgotten their password or triggered an intruder lockout to authenticate with an alternate factor, and repair their own problem, without calling the help desk. It is a common feature in identity management software and often bundled in the same software package as a password synchronization capability.

<span class="mw-page-title-main">Philip Wadler</span> American computer scientist

Philip Lee Wadler is a UK-based American computer scientist known for his contributions to programming language design and type theory. He is the chair of theoretical computer science at the Laboratory for Foundations of Computer Science at the School of Informatics, University of Edinburgh. He has contributed to the theory behind functional programming and the use of monads; and the designs of the purely functional language Haskell and the XQuery declarative query language. In 1984, he created the Orwell language. Wadler was involved in adding generic types to Java 5.0. He is also author of "Theorems for free!", a paper that gave rise to much research on functional language optimization.

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

Matthew Flatt is an American computer scientist and professor at the University of Utah School of Computing in Salt Lake City. He is also the leader of the core development team for the Racket programming language.

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.

Amos Fiat is an Israeli computer scientist, a professor of computer science at Tel Aviv University. He is known for his work in cryptography, online algorithms, and algorithmic game theory.

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

In software engineering, a microservice architecture is an architectural pattern that arranges an application as a collection of loosely coupled, fine-grained services, communicating through lightweight protocols. One of its goals is that teams can develop and deploy their services independently of others. This is achieved by the reduction of several dependencies in the code base, allowing developers to evolve their services with limited restrictions from users, and for additional complexity to be hidden from users. As a consequence, organizations are able to develop software with fast growth and size, as well as use off-the-shelf services more easily. Communication requirements are reduced. These benefits come at a cost to maintaining the decoupling. So, microservice architecture can be a good choice only if the application is too complex to manage as a monolith. Interfaces need to be designed carefully and treated as a public API. One technique that is used is having multiple interfaces on the same service, or multiple versions of the same service, so as to not disrupt existing users of the code.

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

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.

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.

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, 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
  20. ↑ Shen, Gan; Kashiwa, Shun; Kuper, Lindsey (2023-08-31). "HasChor: Functional Choreographic Programming for All (Functional Pearl)". HasChor. 7 (ICFP): 207:541–207:565. doi:10.1145/3607849.
  21. ↑ 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.