Chorégraphies dans le Monde Réel

Since the early days of the Internet, distributed software applications have become one of the leading forces behind the development and economic growth of our society. Nonetheless, the practice of programming distributed systems is one of the most error-prone. Developers strive to correctly implement separate components that, put together, enact an agreed protocol. If one component fails to follow such protocol, it could lead to system blocks or misbehaviours. Ensuring that all components correctly follow the intended protocol is very difficult due to the inherent non-determinism of distributed programs.This led practitioners and theoretical researchers to explore new tools to assist the development of distributed systems. Choreographies are one of these tools. They have been introduced to describe from a global viewpoint the exchange of messages among the components of a distributed system. Moreover, since they describe atomic communications (not split into I/Os), they are free from deadlocks and race conditions by design. Recent theoretical results proved that it is possible to define proper Endpoint Projection (EPP) functions to compile choreographic specifications into their single components. Since EPPs are behaviour preserving, projected systems also enjoy freedom from deadlocks and races by construction. Some of these results have been implemented, however much work has to be done to make choreographies a suitable tool for real-world programming.Aim of this PhD is to formalise non-trivial features of distributed systems with choreographies and to translate our theoretical results into the practice of implemented systems. To this purpose, we provide two main contributions.The first contribution tackles one of the most challenging features of distributed development: programming correct and consistent runtime updates of distributed systems. There is no affirmed technology for structuring runtime updates of distributed applications. Moreover, the non-determinism of distributed systems easily leads to partial applicationsof updates and to inconsistent systems. Our solution is a theoretical model of dynamic choreographies, called DIOC. DIOC provides a clear definition of which components and behaviours can be updated. We prove that systems compiled from a DIOC definition are correct and consistent after any update. Finally, we refine our theoretical model with constructs for a finer control over updates. On this refinement, we develop a framework for programming adaptable distributed systems, called AIOCJ.The second contribution covers one of the main issues of implementing theoretical results on choreographies: formalising the compilation from choreographies to executable programs. There is a sensible departure between choreographic frameworks like Chor (the first on this paradigm) and AIOCJ and their theoretical models: their theories abstract communications with synchronisation on names (a la CCS/π-calculus) yet they compile to Jolie programs, an executable language that uses correlation — a renowned technology of Service-Oriented Computing — for message routing. This discontinuity breaks the chain of proven correctness from choreographies to implemented systems. Our solution is a theory of Applied Choreographies (AC) that models correlation-based message passing. With AC, we formalise the key theoretical problems and the guiding principles that developers should follow to obtain correct implementations. Finally, we prove our approach by defining a correct compiler from AC to the calculus behind the Jolie language.Depuis les débuts de l'Internet, les applications logicielles distribuées sont devenues l'une des forces principales dudéveloppement et de la croissance économique de notre société. Néanmoins, la programmation des systèmes distribués est typiquement difficile, les erreurs y étant nombreuses et compliqués à détecter. Les programmeurs s'efforcent d'implémenter correctement des composants séparés qui, rassemblés, agissent selon un protocole convenu. Si un composant nerespecte pas le protocole, il pourrait bloquer le système ou le faire mal se comporter. S'assurer que tous les éléments suivent correctement le protocole voulu est très difficile à cause du non-déterminisme inhérent des programmes distribués.Cela a amené les programmeurs et les chercheurs à explorer de nouveaux outils pour aider au développement des systèmes distribués. Les chorégraphies sont l'un de ces outils. Elles ont été introduites pour décrire d'un point de vue global leséchanges de messages entre les composants d'un système distribué. De plus, comme elles décrivent des communications atomiques (et non composées d'entrées/sorties), elles sont, par construction, libres de tous blocages (deadlocks) et de situations de compétitions (race conditions). Des résultats théoriques récents prouvent qu'il est possible de définir des fonctions, nommés de Endpoint Projection (EPP), pour compiler les spécifications chorégraphiques vers leur composantes individuelles. Comme les EPPs préservent les comportements, ces composantes individuelles sont elles mêmes libres de blocages et de compétitions. Certains de ces résultats ont été implémentés, mais il reste encore beaucoup de travail pour faire des chorégraphies un outil qui convient à la programmation sur le terrain.Le but de cette thèse est de formaliser les caractéristiques non triviales des systèmes distribués avec les chorégraphies et de traduire nos résultats théoriques vers la pratique des systèmes implémentés. À cette fin, cette thèse apporte deux principales contributions.La première aborde un des problèmes les plus difficiles de la programmation distribuée: le développement de systèmes qui modifient leur propre comportement en cours d'exécution, d'une manière correcte et cohérente. En fait, il n'y a pas de standard pour structurer cette mise à jour d'applications distribuées en cours d'exécution. En outre, le non-déterminisme des systèmes distribués conduit facilement à des mises à jour partielles et donc à des systèmes incohérents. Cette thèse présente un modèle théorique, nommé Dynamic Choreographies, qui permet une définition claire de quels composantset comportements du système distribué peuvent être mise à jour. Nous prouvons que les systèmes compilés à partir d'une définition chorégraphique sont corrects et cohérents après chaque mise à jour. Enfin, nous raffinons notre modèle théorique avec des constructions rendant possible un contrôle plus précis sur les mises à jour. Sur ce raffinement, nous implémentons un cadre pour la programmation de systèmes adaptatifs distribués.La deuxième contribution couvre un des principaux problèmes de l’implémentation des résultats théoriques sur les chorégraphies: la formalisation de la compilation des chorégraphies à des programmes exécutables. Les implémentations actuelles de langages chorégraphiques se distancient considérablement de leurs modèles théoriques: en théorie, les communications sont abstraites au moyen de la synchronisation sur les noms (comme dans le CCS et le pi-calcul), alors qu'en pratique elles sont implémentées après compilation avec différentes politiques d'échange de messages, par exemple, en utilisant les données contenues dans les messages pour leur routage --- une technique appelée ``corrélation'' et typique du Service-Oriented Computing. La discontinuité entre implémentations et modèles théoriques rompt la chaîne de preuve de correction des chorégraphie aux systèmes implémentés. Ce thèse présente un modèle, nommé Applied Choreographies, quiformalise au niveau chorégraphique les politiques réelles des échanges des messages, en particulier ceux de la corrélation.Nous utilisons le modèle des Applied Choreographies pour identifier les problèmes théoriques fondamentaux et nous formalisons les principes à suivre pour le développement de d'implémentations correctes. Enfin, nous démontrons l'applicabilité de notre approche en définissant un compilateur prouvé correct des Applied Choreographiesvers le calcul sur lequel est fondé le langage Jolie