Thèse de Claire Soyez-Martin

De la théorie des semigroupes à la vectorisation : valider les langages réguliers

L'évaluation efficace des expressions régulières constitue un défi persistant depuis de nombreuses décennies. Au fil du temps, des progrès substantiels ont été réalisés grâce à une variété d'approches, allant de nouveaux et ingénieux algorithmes à des optimisations complexes de bas niveau. Les outils de pointe de ce domaine utilisent ces techniques d'optimisation, et repoussent constamment les limites de leur efficacité. Une avancée notoire réside dans l'intégration de la vectorisation, qui exploite une forme de parallélisme de bas niveau pour traiter l'entrée par blocs, entraînant ainsi d'importantes améliorations de performances. Malgré une recherche approfondie sur la conception d'algorithmes sur mesure pour des tâches particulières, ces solutions manquent souvent de généralisabilité, car la méthodologie sous-jacente à ces algorithmes ne peut pas être appliquée de manière indiscriminée à n'importe quelle expression régulière, ce qui rend difficile son intégration dans les outils existants. Cette thèse présente un cadre théorique permettant de générer des programmes vectorisés particuliers capables d'évaluer les expressions régulières correspondant aux expressions rationnelles appartenant à une classe logique donnée. L'intérêt de ces programmes vectorisés vient de l'utilisation de la théorie algébrique des automates, qui offre certains outils algébriques permettant de traiter les lettres en parallèle. Ces outils permettent également d'analyser les langages réguliers plus finement, offrent accès à des optimisations des programmes vectorisés basées sur les propriétés algébriques de ces langages. Cette thèse apporte des contributions dans deux domaines. D'une part, nous présentons des implémentations et des benchmarks préliminaires, afin d'étudier les possibilités offertes par l'utilisation de l'algèbre et de la vectorisation dans les algorithmes d'évaluation des expressions régulières. D'autre part, nous proposons des algorithmes capables de générer des programmes vectorisés reconnaissant les langages apparenant à deux classes d'expressions rationnelles, la logique du premier ordre et sa restriction aux formules utilisant au plus deux variables.

Jury

M. Sylvain SALVATI Cristal, Université de Lille Directeur de thèse. M. Damien POUS LIP, École Normale Supérieure Rapporteur. M. Sylvain SCHMITZ IRIF, Université Paris Cité Rapporteur. Mme Sophie TISON Cristal, Université de Lille Examinatrice. Mme Tatiana STARIKOVSKAYA DI/ENS, École normale supérieure, Paris Examinatrice. M. Pierre SENELLART DI/ENS, École normale supérieure, Paris Examinateur. M. Michaël HAUSPIE Cristal, Université de Lille Co-directeur de thèse. M. Charles PAPERMAN Cristal, Université de Lille Examinateur. .

Thèse des équipes 2XS et LINKS soutenue le 14/12/2023