Choreographic Programming

Research output: Book/anthology/thesis/reportPh.D. thesisResearch

Abstract

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.
Original languageEnglish
Place of PublicationIT University of Copenhagen
ISBN (Print)978-87-7949-299-8
Publication statusPublished - 2013

Fingerprint

Hazards and race conditions
Formal logic
Distributed computer systems
Computer programming
Computer programming languages
Concretes
Specifications
Network protocols

Cite this

Montesi, F. (2013). Choreographic Programming. IT University of Copenhagen.
Montesi, Fabrizio. / Choreographic Programming. IT University of Copenhagen, 2013.
@phdthesis{9a3ddf2dbba544adb61449fbdb1d25dd,
title = "Choreographic Programming",
abstract = "Choreographies are descriptions of distributed systems where the developer gives a globalview of how messages are exchanged by endpoint nodes (endpoints for short), instead ofseparately defining the behaviour of each endpoint. They have a significant impact on thequality 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 developmentof programming languages, giving rise to a programming paradigm that in this dissertationwe 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 typicalsafety problems such as deadlocks and race conditions; the concrete implementation ofeach endpoint described in a choreography can then be automatically obtained by compilation, ensuring that such implementations are also safe by construction from the originatingchoreography. However, current formal models for choreographies do not deal with criticalaspects of distributed programming, such as asynchrony, mobility, modularity, and multiparty sessions; it remains thus unclear whether choreographies can still guarantee safetywhen dealing with such nontrivial features.This PhD dissertation argues for the usefulness of choreographic programming as aparadigm for the development of safe distributed systems. We proceed by investigating itsfoundations 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 todistributed implementations in terms of a variant of the π-calculus, the reference model formobile 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 thatLCL 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 inLCL correspond to choreographies; and (ii) the transformations between proofs in LCL toproofs 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 frameworkfor choreographic programming, called Chor. Chor provides an Integrated DevelopmentEnvironment (IDE) for programming with choreographies, equipped with a type checkerfor verifying that choreographies respect protocol specifications given as session types.Programs in Chor can be compiled to executable endpoint implementation in the Jolieprogramming language, a general-purpose language for distributed computing, which weextend to support the development of multiparty asynchronous sessions. We use Chor forevaluating choreographic programming against a series of use cases.",
author = "Fabrizio Montesi",
year = "2013",
language = "English",
isbn = "978-87-7949-299-8",

}

Montesi, F 2013, Choreographic Programming. IT University of Copenhagen.

Choreographic Programming. / Montesi, Fabrizio.

IT University of Copenhagen, 2013.

Research output: Book/anthology/thesis/reportPh.D. thesisResearch

TY - BOOK

T1 - Choreographic Programming

AU - Montesi, Fabrizio

PY - 2013

Y1 - 2013

N2 - Choreographies are descriptions of distributed systems where the developer gives a globalview of how messages are exchanged by endpoint nodes (endpoints for short), instead ofseparately defining the behaviour of each endpoint. They have a significant impact on thequality 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 developmentof programming languages, giving rise to a programming paradigm that in this dissertationwe 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 typicalsafety problems such as deadlocks and race conditions; the concrete implementation ofeach endpoint described in a choreography can then be automatically obtained by compilation, ensuring that such implementations are also safe by construction from the originatingchoreography. However, current formal models for choreographies do not deal with criticalaspects of distributed programming, such as asynchrony, mobility, modularity, and multiparty sessions; it remains thus unclear whether choreographies can still guarantee safetywhen dealing with such nontrivial features.This PhD dissertation argues for the usefulness of choreographic programming as aparadigm for the development of safe distributed systems. We proceed by investigating itsfoundations 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 todistributed implementations in terms of a variant of the π-calculus, the reference model formobile 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 thatLCL 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 inLCL correspond to choreographies; and (ii) the transformations between proofs in LCL toproofs 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 frameworkfor choreographic programming, called Chor. Chor provides an Integrated DevelopmentEnvironment (IDE) for programming with choreographies, equipped with a type checkerfor verifying that choreographies respect protocol specifications given as session types.Programs in Chor can be compiled to executable endpoint implementation in the Jolieprogramming language, a general-purpose language for distributed computing, which weextend to support the development of multiparty asynchronous sessions. We use Chor forevaluating choreographic programming against a series of use cases.

AB - Choreographies are descriptions of distributed systems where the developer gives a globalview of how messages are exchanged by endpoint nodes (endpoints for short), instead ofseparately defining the behaviour of each endpoint. They have a significant impact on thequality 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 developmentof programming languages, giving rise to a programming paradigm that in this dissertationwe 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 typicalsafety problems such as deadlocks and race conditions; the concrete implementation ofeach endpoint described in a choreography can then be automatically obtained by compilation, ensuring that such implementations are also safe by construction from the originatingchoreography. However, current formal models for choreographies do not deal with criticalaspects of distributed programming, such as asynchrony, mobility, modularity, and multiparty sessions; it remains thus unclear whether choreographies can still guarantee safetywhen dealing with such nontrivial features.This PhD dissertation argues for the usefulness of choreographic programming as aparadigm for the development of safe distributed systems. We proceed by investigating itsfoundations 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 todistributed implementations in terms of a variant of the π-calculus, the reference model formobile 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 thatLCL 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 inLCL correspond to choreographies; and (ii) the transformations between proofs in LCL toproofs 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 frameworkfor choreographic programming, called Chor. Chor provides an Integrated DevelopmentEnvironment (IDE) for programming with choreographies, equipped with a type checkerfor verifying that choreographies respect protocol specifications given as session types.Programs in Chor can be compiled to executable endpoint implementation in the Jolieprogramming language, a general-purpose language for distributed computing, which weextend to support the development of multiparty asynchronous sessions. We use Chor forevaluating choreographic programming against a series of use cases.

M3 - Ph.D. thesis

SN - 978-87-7949-299-8

BT - Choreographic Programming

CY - IT University of Copenhagen

ER -

Montesi F. Choreographic Programming. IT University of Copenhagen, 2013.