Un modèle de concurrence fondé sur les interprètes monadiques : Sémantique exécutable pour un sous-ensemble concurrent de LLVM IR

Les interprètes monadiques sont un outil puissant pour modéliser et raisonner sur les langages de programmation du premier ordre. Une approche monadique permet de définir une sémantique modulaire, composable et exécutable. En particulier, le projet Vellvm utilise la structure de données d'Interaction Trees (arbres d'interaction) pour formaliser la sémantique du code LLVM IR séquentiel dans le prouveur Rocq. Cette thèse s'inscrit dans l'objectif d'étendre ce travail à la concurrence, à travers deux contributions principales.Premièrement, nous proposons une structure d'arbre sous-jacente révisée, les Choice Trees (arbres de choix), une variante des Interaction Trees avec un nouveau type de nœud qui représente le choix non-déterministe. Cet ajout a beaucoup d'implications méta-théoriques, notamment sur la notion d'interprétation de Choice Trees. Nous étudions donc en profondeur les techniques de preuve coinductives sur les Choice Trees, en nous concentrant sur la théorie équationnelle de notions de raffinement et d'équivalence de programme fondées sur des simulations et bisimulations. Deuxièmement, nous tirons avantage de cette nouvelle structure de Choice Trees pour modéliser la sémantique d'un sous-ensemble concurrent de LLVM IR. Notre sémantique est construite en couches successives, qui interprètent chaque aspect de la sémantique séparément : les accès à des variables, la gestion des fils d'exécution, et les accès à la mémoire. Grâce à la modularité de l'approche, il est possible de changer de modèle mémoire (ou de langage source) en modifiant une seule de ces passes d'interprétation. En particulier, nous proposons trois modèles mémoire différents : un modèle mémoire inspiré de Promising, un modèle mémoire de type Total Store Ordering, et un modèle mémoire fort de cohérence séquentielle. En exploitant les résultats sur les notions de (bi)similarité des Choice Trees, nous établissons la théorie équationnelle de nos constructions et montrons comment transporter des résultats d'équivalence à travers les différentes couches de notre sémantique. Enfin, notre modèle est exécutable, la sémantique peut donc être testée par extraction vers OCaml.