Varda : a language for programming distributed systems by composition

Varda : un langage pour la programmation de systèmes distribués par composition Les grands systèmes distribués sont souvent construits en assemblant des composants prêts à l’emploi (OTS), c’est-à-dire des composants, des services, des processus, etc., développés indépendamment. La pratique actuelle consiste à interconnecter manuellement leurs API. Cette méthode est ad hoc, complexe, fastidieuse et sujette aux erreurs. Les langages de programmation offrent une approche prometteuse pour résoudre ce problème. Premièrement, ils permettent de réduire l’apparition de bogues. Le développeur spécifie formellement le système. Ensuite, le compilateur assure des garanties de correction et génère une implémentation correcte par construction. Deuxièmement, les langages contribuent à améliorer la productivité des programmeurs. La génération de code automatise l’interconnexion des composants et peut optimiser l’implémentation générée. Dans cette thèse, nous proposons un nouveau langage, Varda, à l’intersection entre langages de programmation et de spécification. Un programme Varda décrit l’interconnexion de composants en une architecture cohérente. Le développeur isole un composant OTS derrière un shield. Celui-ci restreint le comportement du composant en spécifiant son interface, son protocole (c’est-à-dire ce qu’il peut envoyer ou recevoir, et dans quel ordre), ainsi que des pre/post-conditions. Les composants peuvent être logiquement imbriqués. Un composant externe orchestre ses composants internes, en créant ou en tuant des instances, en les interconnectant et en supervisant leurs erreurs ; il peut intercepter et manipuler leurs communications. Varda fournit des garanties solides, grâce à de l’analyse statique et à de l’injection de tests dynamiques. Pour être utile en pratique au développement de systèmes distribués, Varda adopte une approche pragmatique. Un shield peut contenir du code non-Varda (par ex, Java) afin d’incorporer des composants en boîte noire. Varda permet de contrôler les propriétés non fonctionnelles qui sont importantes pour la performance et la tolérance aux pannes, par exemple l’élasticité, le placement et l’intégration. Le compilateur Varda automatise la génération du code d’interconnexion et d’orchestration. Varda prend en charge l’exécution non-stop, grâce à des mécanismes de supervision. Nous démontrons l’expressivité et l’ergonomie de Varda en programmant des structures distribuées classiques (par exemple, le contrôle d’accès). Pour illustrer l’emploi en condition réelle de Varda, nous implémentons un clone du datastore géorépliqué AntidoteDB. Les applications Varda sont compactes et présentent une conception modulaire et réutilisable. Nos expériences montrent que le surcoût d’exécution est modeste, grâce à la vérification et à l’optimisation au moment de la compilation.