Choreographic programming

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

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.

send (credentials, serviceID) to CAS
recv result from CAS

recv result from 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.