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