Choreographic programming: Difference between revisions

Revision as of 10:40, 14 January 2022

Revision as of 15:05, 19 January 2022

Line 5:

== 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'''.<ref name="bt-survey"/>

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

Line 33 ⟶ 35:

In Line 2, the <code>CAS</code> checks if the request is valid for obtaining an authentication token.

If so, it generates a token and communicates a <code>Success</code> message containing the token to both <code>Client</code> and <code>Service</code> (Lines 3–5).

Otherwise, the <code>CAS</code> informs <code>Client</code> and <code>Service</code> that authentication failed, by sending a <code>Failure</code> 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 used as libraries infor software that needs to participate in a computer network. by following a protocol,<ref name="mp-langs" /><ref>[https://www.choral-lang.org/ Choral programming language]</ref> or standalone distributed programs.<ref name=":0" /><ref name="aiocj-paper" />

The translation of a choreography into distributed programs is called '''endpoint projection''' (EPP for short).<ref name="bt-survey" /><ref name="mp-langs" />

Endpoint projection returns a program for each role described in the source choreography.<ref name="mp-langs" /> For example, given the choreography above, endpoint projection would return three programs: one for <code>Client</code>, one for <code>Service</code>, and one for <code>CAS</code>. They are shown below in pseudocode form, where <code>send</code> and <code>recv</code> are primitives for sending and receiving messages to/from other roles.

{| class="wikitable"

|+Endpoint Projection (EPP) of the SSO choreography

!Client

!Service

!CAS

|-

|<syntaxhighlight lang="text" line>

send (credentials, serviceID) to CAS

recv result from CAS

</syntaxhighlight>

|<syntaxhighlight lang="text" line>

recv result from CAS

</syntaxhighlight>

|<syntaxhighlight lang="text" line>

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

</syntaxhighlight>

|}

For each role, its code contains the actions that the role should execute to implement the choreography correctly together with the others.

== Development ==

Line 45 ⟶ 77:

== Languages ==

* AIOCJ ([http://www.cs.unibo.it/projects/jolie/aiocj.html website]).<ref name="aiocj-paper"/> A choreographic programming language for [[Adaptation (computer science)|adaptable systems]] that produces code in in [[Jolie (programming language)|Jolie]].

* Chor ([https://www.chor-lang.org/ website]).<ref name=":0">{{Cite book|chapter-url=https://doi.org/10.1145/2429069.2429101|doi=10.1145/2429069.2429101|chapter=Deadlock-freedom-by-design|title=Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '13|year=2013|last1=Carbone|first1=Marco|last2=Montesi|first2=Fabrizio|page=263|isbn=9781450318327|s2cid=15627190}}</ref> A [[session type|session-typed]] choreographic programming language that compiles to [[microservices]] in [[Jolie (programming language)|Jolie]].

* Choral ([https://www.choral-lang.org/ website]). A higher-order, object-oriented choreographic programming language that compiles to libraries in [[Java (programming language)|Java]].

* Core Choreographies.<ref>{{Cite journal|url=https://doi.org/10.1016/j.tcs.2019.07.005|doi = 10.1016/j.tcs.2019.07.005|title = A core model for choreographic programming|year = 2020|last1 = Cruz-Filipe|first1 = Luís|last2 = Montesi|first2 = Fabrizio|journal = Theoretical Computer Science|volume = 802|pages = 38–66|s2cid = 199122777}}</ref> A core theoretical model for choreographic programming. An implementation is available in [[Coq]].<ref>{{Cite book|url=https://doi.org/10.4230/LIPIcs.ITP.2021.15|doi=10.4230/LIPIcs.ITP.2021.15|isbn=9783959771887|title=Formalising a Turing-Complete Choreographic Language in Coq|series=Leibniz International Proceedings in Informatics (LIPIcs)|year=2021|volume=193|pages=15:1–15:18|last1=Cohen|first1=Liron|last2=Kaliszyk|first2=Cezary|s2cid=231802115}}</ref>