Soutenance de thèse : Arthur NAVARRO

Extraction et projection de chorégraphies pour l'optimisation de services distribués réactifs: un continuum langage - runtime

Doctorant : Arthur NAVARRO

Laboratoire INSA : CITI - Centre d'innovation en Télécommunications et Intégration de Services
École doctorale n°512 lnfoMaths - Informatique et Mathématiques de Lyon

L'essor des grandes architectures distribuées telles que les microservices ou le serverless ces dernières années s'accompagne d'un ensemble de défis. L'augmentation de l'activité réseau due aux communications nécessaires entre les processus peut entraîner une forte pression sur les E/5 réseau et les ressources telles que le temps CPU et l'empreinte mémoire. En outre, si les services individuels sont plus petits et plus faciles à raisonner que les monolithes gonflés, une grande application distribuée peut s'étendre sur des dizaines, des centaines ou des milliers de services fortement dépendants des communications. La probabilité de bogues ou d'erreurs de programmation simultanés augmente, de même que la difficulté d'identifier et de corriger ces bogues. Ces deux problèmes ne sont pas orthogonaux, car l'efficacité des ressources peut être optimisée par l'utilisation de langages non bloquants et asynchrones qui peuvent en retour obscurcir le flux d'exécution et le cycle de vie des différents composants. Pour relever ces défis, nous avons identifié deux approches complémentaires: la vérification du système et la conception du langage. Aujourd'hui, les types de sessions multipartites et la programmation chorégraphique sont en train d'envahir les langages de programmation courants. La programmation chorégraphique peut être considérée comme un cadre permettant de construire des systèmes sans blocage en réifiant le fonctionnement d'une application comprenant de nombreux processus en un seul objet : une chorégraphie globale. Dans la pratique, les programmeurs écrivent souvent des systèmes distribués en spécifiant le comportement des composants individuels, c'est-à-dire par le biais de chorégraphies locales. Reconstruire une chorégraphie globale cohérente à partir de ces vues locales, afin de vérifier les propriétés globales, est une tâche difficile. Cette difficulté provient en particulier du fait que les langages conçus pour exprimer des chorégraphies globales modélisent généralement la communication comme un échange de données synchrone, et que les cadres actuels ne prennent pas en charge la vérification dans des contextes asynchrones. Nous avons conçu un compilateur capable de transformer des chorégraphies locales en microservices Java en utilisant des bibliothèques réactives existantes, ainsi qu'un analyseur de chorégraphies locales capable de valider des propriétés dans des réseaux de milliers de chorégraphies locales. Même si l'analyse est effectuée sur des chorégraphies locales, la liberté de deadlock, la liberté de livelock, les branches inaccessibles sont des propriétés vérifiées globales : en tant que tel, l'analyseur a besoin d'un ensemble complet de chorégraphies locales pour raisonner sur l'ensemble de l'application. De plus, nous avons caractérisé l'analyseur en termes de complexité algorithmique et de temps de traitement en fonction de la taille et de la complexité des réseaux considérés. Notre approche est un pas vers l'unification des types de session et de la programmation chorégraphique dans un cadre unique, permettant la vérification des processus synchrones et asynchrones, ainsi que l'offre de perspectives locales et globales sur une application distribuée lorsque cela est possible. En combinant l'analyse formelle des chorégraphies locales avec des aperçus pratiques du comportement du langage en cours d'exécution, nous montrons que, même si la vérification formelle est théoriquement complexe, elle peut être rendue tractable et efficace en pratique grâce à des heuristiques, tandis que les optimisations au niveau du langage et des bibliothèques, bien que transparentes et légères, peuvent être complexes à mettre en œuvre, et produisent souvent des améliorations de performance limitées.