Follow with Edit this page on Go back to the Bliki index

Choreographic Language

By Fabrizio Montesi. Created on 2023-05-17. Last updated on 2024-07-25.
See also: Introduction to Choreographies

Table of Contents (click to show)

A choreographic language is a language for expressing choreographies [Montesi 2023]. Key to choreographic languages is having a high-level primitive for expressing a communication between independent processes (also called roles, or participants). This is inspired by the 'Alice and Bob' notation of security protocols, which presents the primitive

A -> B: M

for expressing the communication of a message M from A (Alice) to B (Bob) [Needham and Schroeder 1978].

Choreographic languages can be roughly divided in two categories:

Choreographic languages meant to express computer programs. These languages typically include primitives for expressing computation, as often found in distributed applications, security protocols, etc. They are called choreographic programming languages.
Choreographic languages without computation, aimed at expressing abstract specifications of protocols. Notable examples include global types, BPMN choreographies, and (at least in the way they are typically applied) sequence diagrams.

Another possible source of categorisation: choreographic languages can be textual, graphical, or visual. Some examples are given next. In the remainder, p, q, r, s, etc. are process names.

Choreographic languages can be translated to executable distributed code or abstract models of participants by means of endpoint projection.

Recursive Choreographies

An example of a choreographic language is the language of Recursive Choreographies [Montesi 2023]. I often refer to it examples in the other entries.

Recursive Choreographies is defined by the following grammar, in BNF format (the original presentation is adapted to ASCII here). Note that, in the examples on these pages, I sometimes take the liberty of omitting trailing 0s and else branches.

(Choreographies)	C ::=	I;C							(sequence)
						|	0							(empty choreography)

(Instructions)		I ::=	p.e -> q.x					(value communication)
						|	p -> q[L]					(selection)
						|	p.x := e					(assignment)
						|	if p.e then C1 else C2		(conditional)
						|	X(p...)						(procedure call)

(Expressions)		e ::=	v							(value)
						|	x							(variable)
						|	f(e...)						(function call)

The syntax of Recursive Choreographies [Montesi 2023].

In the syntax, p ranges over process names, L over selection labels (special ), X ranges over procedure names, v ranges over (data) values, x ranges over local variables, and f ranges over function names that are assumed to be defined in a separate language. Each process is assumed to have a local memory store that maps variables to values.

A choreography C is essentially a list of instructions (I), terminated by 0. Instructions can be read as follows.

p.e -> q.x reads 'p locally evalutes e and communicates the resulting value to q, which stores the value in its local variable x.
p -> q[L] reads 'p communicates the selection label L to q'. See knowledge of choice about the role of selections.
p.x := e reads 'p locally evaluates e and stores the result in its variable x'.
if p.e then C1 else C2 reads 'if p evaluates e to the value true, proceed as C1, otherwise as C2'.
X(p...) means 'the processes p... enter procedure X'. p... stands for a list of process names, e.g., p, q, r. Procedures are mapped to choreographies in a context of procedure definitions, and can be recursive.

Choreographic Programming Languages

A choreographic programming language is a choreographic language for expressing executable concurrent and distributed code [Montesi 2013]. See choreographic programming. Recursive Choreographies is a choreographic programming language.

Global Types

Global types are choreographies where communications define propositions about the transmitted data, instead of the computations used to produce or manipulate the data [Honda et al. 2016]. They are often used in theories of static verification for process calculi called multiparty session types [Honda et al. 2016; Hüttel et al. 2016].

Languages for global types are typically similar to Recursive Choreographies, with some notable key differences:

Value communication specifies the type of the transmitted message (e.g., an integer), instead of the expression and variable used for computing and storing the message.
There is no assignment instruction.
Conditionals are nondeterministic choices, e.g., C1 + C2.

Sequence Diagrams

Sequence diagram are visualisations of choreographies, where the timelines of participants are represented by vertical lines and their interactions by connecting horisontal lines. See sequence diagrams on Wikipedia.

Tools for sequence diagrams typically give a lot of freedom in what can be written about interactions, so the choice of including computation or not can be left to the user.

References

Honda, K., Yoshida, N., Carbone, M. [2016], 'Multiparty Asynchronous Session Types', J. ACM 63(1): 9:1-9:67. https://doi.org/10.1145/2827695

Hüttel, H., Lanese, I., Vasconcelos, V. T., Caires, L., Carbone, M., Deniélou, P., Mostrous, D., Padovani, L., Ravara, A., Tuosto, E., Vieira, H. T., Zavattaro, G. [2016], 'Foundations of Session Types and Behavioural Contracts', ACM Comput. Surv. 49(1): 3:1-3:36. https://doi.org/10.1145/2873052

Montesi, F. [2013], 'Choreographic Programming', PhD Thesis, IT University of Copenhagen. https://www.fabriziomontesi.com/files/choreographic-programming.pdf

Montesi, F. [2023], 'Introduction to Choreographies', Cambridge University Press. https://doi.org/10.1017/9781108981491

Needham, Roger M., Schroeder, Michael D. [1978], 'Using Encryption for Authentication in Large Networks of Computers', Commun. ACM 21(12): 993-999. https://doi.org/10.1145/359657.359659