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 used in the development of programming languages, giving rise to a programming paradigm that in this dissertation we refer to as Choreographic Programming.
Recent studies show that choreographies 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 generated, ensuring that such implementations are safe by construction. 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 suitability 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 for choreographic programming that supports asynchrony, mobility, modularity, and multiparty sessions. In the model, choreographies are projected to distributed endpoint code in terms of the π-calculus. Projection 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), an extension of linear logic. We propose a Curry-Howard correspondence between LCL and a calculus of choreographies, proving that: (i) proofs in LCL correspond to choreographies; and (ii) proof transformations in LCL yield procedures for compiling choreographies to endpoint programs 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 framework for choreographic programming, called Chor. Chor provides an Integrated Development Environment (IDE) for programming with choreographies, equipped with a type checker for verifying their correctness based on our formal development. Programs in Chor can be compiled to executable endpoint code in Jolie, a language for distributed programming. We use Chor for evaluating choreographic programming against a series of use cases.
Recent studies show that choreographies 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 generated, ensuring that such implementations are safe by construction. 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 suitability 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 for choreographic programming that supports asynchrony, mobility, modularity, and multiparty sessions. In the model, choreographies are projected to distributed endpoint code in terms of the π-calculus. Projection 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), an extension of linear logic. We propose a Curry-Howard correspondence between LCL and a calculus of choreographies, proving that: (i) proofs in LCL correspond to choreographies; and (ii) proof transformations in LCL yield procedures for compiling choreographies to endpoint programs 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 framework for choreographic programming, called Chor. Chor provides an Integrated Development Environment (IDE) for programming with choreographies, equipped with a type checker for verifying their correctness based on our formal development. Programs in Chor can be compiled to executable endpoint code in Jolie, a language for distributed programming. We use Chor for evaluating choreographic programming against a series of use cases.
| Original language | English |
|---|
| Publisher | IT-Universitetet i København |
|---|---|
| Number of pages | 275 |
| ISBN (Print) | 978-87-7949-299-8 |
| Publication status | Published - 2014 |
| Series | ITU-DS |
|---|---|
| Number | 104 |
| ISSN | 1602-3536 |