Choreographic Programming
Fabrizio Montesi
[2013].
PhD Thesis, IT University of Copenhagen.
Choreographies are descriptions of distributed systems where the developer gives a global view of how messages are exchanged by endpoint nodes (endpoints for short), instead of separately defining the behaviour of each endpoint. They have a significant impact on the quality of software, as they offer a concise view of the message flows enacted by a system. For this reason, in the last decade choreographies have been employed in the development of programming languages, giving rise to a programming paradigm that in this dissertation we refer to as Choreographic Programming.
Recent formal investigations of choreographies show that they have potential as foundations for the development of safe distributed software. The key idea is that since choreographies abstract from the single input/output actions of endpoints, they avoid typical safety problems such as deadlocks and race conditions; the concrete implementation of each endpoint described in a choreography can then be automatically obtained by compilation, ensuring that such implementations are also safe by construction from the originating choreography. However, current formal models for choreographies do not deal with critical aspects of distributed programming, such as asynchrony, mobility, modularity, and multiparty sessions; it remains thus unclear whether choreographies can still guarantee safety when dealing with such nontrivial features.
This PhD dissertation argues for the usefulness of choreographic programming as a paradigm for the development of safe distributed systems. We proceed by investigating its foundations and application. To this aim we provide three main contributions.
The first contribution is the development of a formal model and type theory for choreographic programming that support asynchrony, mobility, modular development, and multiparty sessions. We prove that our model guarantees safety by mapping choreographies to distributed implementations in terms of a variant of the π-calculus, the reference model for mobile processes. Our translation preserves the expected safety properties of choreographies, among which freedom from deadlocks and race conditions.
The second contribution is the development of Linear Connection Logic (LCL), a formal logic that captures the reasoning behind choreographic programming. We show that LCL is a conservative extension of Linear Logic. We then develop a Curry-Howard correspondence between LCL and a calculus of choreographies, proving that: (i) proofs in LCL correspond to choreographies; and (ii) the transformations between proofs in LCL to proofs in Linear Logic and vice versa correspond to compiling choreography programs to π-calculus terms and vice versa. The latter result, known as round-trip development, contributes to the open problem of extracting choreographies from existing endpoint programs.
The third contribution is the implementation of a prototype programming framework for choreographic programming, called Chor. Chor provides an Integrated Development Environment (IDE) for programming with choreographies, equipped with a type checker for verifying that choreographies respect protocol specifications given as session types. Programs in Chor can be compiled to executable endpoint implementation in the Jolie programming language, a general-purpose language for distributed computing, which we extend to support the development of multiparty asynchronous sessions. We use Chor for evaluating choreographic programming against a series of use cases.
@PhdThesis{M13:phd,
author = "Fabrizio Montesi",
title = "Choreographic {P}rogramming",
school = "IT University of Copenhagen",
type = "Ph.{D}. Thesis",
year = 2013,
note = {\url{https://www.fabriziomontesi.com/files/choreographic-programming.pdf}}
}A PDF is available (possibly a preprint):