Choreographic programming
In computer science, choreographic programming is a programming paradigm where programs are compositions of interactions among multiple concurrent participants.[1][2][3]
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:
Client
, which wishes to obtain an access token fromCAS
to interact withService
.Service
, which needs to know fromCAS
if theClient
should be given access.CAS
, which is the Central Authentication Service responsible for checking theClient
'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,[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.
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
Languages
- AIOCJ (website).[6] A choreographic programming language for adaptable systems that produces code in Jolie.
- Chor (website).[5] A session-typed choreographic programming language that compiles to microservices in Jolie.
- Choral (website). A higher-order, object-oriented choreographic programming language that compiles to libraries in Java.
- Core Choreographies.[16] A core theoretical model for choreographic programming. A mechanised implementation is available in Coq.[17][18][19]
- Kalas.[20] A choreographic programming language with a verified compiler to CakeML.
- Pirouette.[8] A mechanised choreographic programming language theory with higher-order procedures.
See also
- Security protocol notation
- Sequence diagram
- Service choreography
- Structured concurrency
- Multitier programming
References
- ^ S2CID 102335067.
- ^ hdl:10044/1/44282.
- ^
- ^ Choral programming language
- ^ S2CID 15627190.
- ^ S2CID 5555662.
- ^
- ^ Arend Rensink (2015-08-30). "Fabrizio Montesi wins the EAPLS Best PhD Dissertation Award 2014". European Association for Programming Languages and Systems.
- S2CID 15737118.
- S2CID 32617923.
- S2CID 18067252.
- S2CID 39112346.
- S2CID 12872876.
- S2CID 53015580.
- S2CID 199122777.
- S2CID 231802115.
- S2CID 252090305.
- S2CID 231985665, retrieved 2022-03-07
- S2CID 251322644.