HOME

TheInfoList



OR:

In
computer science Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to practical disciplines (includin ...
, choreographic programming is a
programming paradigm Programming paradigms are a way to classify programming languages based on their features. Languages can be classified into multiple paradigms. Some paradigms are concerned mainly with implications for the execution model of the language, s ...
where programs are compositions of interactions among multiple
concurrent Concurrent means happening at the same time. Concurrency, concurrent, or concurrence may refer to: Law * Concurrence, in jurisprudence, the need to prove both ''actus reus'' and ''mens rea'' * Concurring opinion (also called a "concurrence"), a ...
participants.(ECOOP 2021 Distinguished Paper)
/ref>


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. Choreographic languages are inspired by
security protocol notation 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 c ...
(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". Alice, Bob, etc. are typically called roles or processes. The example below shows a choreography for a simplified
single sign-on Single sign-on (SSO) is an authentication scheme that allows a user to log in with a single ID to any of several related, yet independent, software systems. True single sign-on allows the user to log in once and access services without re-enterin ...
(SSO) protocol based on a
Central Authentication Service The Central Authentication Service (CAS) is a single sign-on protocol for the web. Its purpose is to permit a user to access multiple applications while providing their credentials (such as user ID and password) only once. It also allows web appl ...
(CAS) that involves three roles: * Client, which wishes to obtain an
access token In computer systems, an access token contains the security credentials for a login session and identifies the user, the user's groups, the user's privileges, and, in some cases, a particular application. In some instances, one may be asked to en ...
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 The Central Authentication Service (CAS) is a single sign-on protocol for the web. Its purpose is to permit a user to access multiple applications while providing their credentials (such as user ID and password) only once. It also allows web appl ...
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, 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.(EAPLS Best PhD Dissertation Award)
/ref>(POPL 2022 Distinguished Paper)
/ref> The inspiration for the syntax of choreographic programming languages can be traced back to
security protocol notation 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 c ...
, also known as "Alice and Bob" notation. 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 In computer science, the process calculi (or process algebras) are a diverse family of related approaches for formally modelling concurrent systems. Process calculi provide a tool for the high-level description of interactions, communications, and ...
. Choreographic programming is an active area of research. The paradigm has been used in the study of
information flow In discourse-based grammatical theory, information flow is any tracking of referential information by speakers. Information may be ''new,'' just introduced into the conversation; ''given,'' already active in the speakers' consciousness; or ''old ...
, parallel computing,
cyber-physical system A cyber-physical system (CPS) or intelligent system is a computer system in which a mechanism is controlled or monitored by computer-based algorithms. In cyber-physical systems, physical and software components are deeply intertwined, able to ope ...
s, runtime adaptation, and
system integration System integration is defined in engineering as the process of bringing together the component sub- systems into one system (an aggregation of subsystems cooperating so that the system is able to deliver the overarching functionality) and ensuring ...
.


Languages

* AIOCJ
website
. A choreographic programming language for adaptable systems that produces code in Jolie. * Chor
website
. A session-typed choreographic programming language that compiles to
microservices A microservice architecture – a variant of the service-oriented architecture structural style – is an architectural pattern that arranges an application as a collection of loosely-coupled, fine-grained services, communicating through ligh ...
in Jolie. * Choral
website
. A higher-order, object-oriented choreographic programming language that compiles to libraries in
Java Java (; id, Jawa, ; jv, ꦗꦮ; su, ) is one of the Greater Sunda Islands in Indonesia. It is bordered by the Indian Ocean to the south and the Java Sea to the north. With a population of 151.6 million people, Java is the world's mo ...
. * Core Choreographies. A core theoretical model for choreographic programming. A
mechanised Mechanization is the process of changing from working largely or exclusively by hand or with animals to doing that work with machinery. In an early engineering text a machine is defined as follows: In some fields, mechanization includes the ...
implementation is available in Coq. * Kalas. A choreographic programming language with a verified compiler to CakeML. * Pirouette. A
mechanised Mechanization is the process of changing from working largely or exclusively by hand or with animals to doing that work with machinery. In an early engineering text a machine is defined as follows: In some fields, mechanization includes the ...
choreographic programming language theory with higher-order procedures.


See also

*
Security protocol notation 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 c ...
*
Sequence diagram A sequence diagram or system sequence diagram (SSD) shows process interactions arranged in time sequence in the field of software engineering. It depicts the processes involved and the sequence of messages exchanged between the processes needed ...
* Service choreography * Structured concurrency * Multitier programming


References

{{Reflist


External links


www.choral-lang.org
Concurrent computing Programming paradigms