HDR de Baptiste Lepers

"Cette habilitation présente plusieurs contributions dans le domaine des systèmes d’exploitation, avec un accent particulier sur la détection de bugs dans des environnements concurrents et l’optimisation des performances sur des infrastructures modernes.

 

Dans un premier volet, j’ai développé une nouvelle approche pour inférer les interactions concurrentes dans des programmes multithreadés sans verrou. J’ai proposé une heuristique novatrice basée sur l’appariement des barrières mémoire, permettant de détecter des fonctions potentiellement concurrentes dans des contextes dépourvus de verrous explicites. En appliquant cette méthode au noyau Linux, j’ai découvert 12 bugs critiques qui menaçaient la stabilité et l’intégrité des données, et dont les correctifs ont été intégrés depuis la version 5.15.

 

Un second volet explore les limites des bases de données Key-Value (KV) sur les systèmes de stockage NVMe SSD modernes. Nous avons conçu KVell, un nouveau KV exploitant pleinement les capacités de ces disques, éliminant les limitations dues au CPU qui affectent les KVs existants. KVell, basé sur une architecture sans partage, permet des performances de lecture et d’écriture significativement plus rapides, surpassant l’état de l’art avec des gains de 2× en lecture et 5× en écriture.

 

Enfin, mon travail sur l’ordonnancement des tâches dans Linux a révélé des inefficacités majeures sur les architectures multicœurs, où certains cœurs étaient systématiquement sous-utilisés. J’ai corrigé ces défauts, conduisant à des améliorations significatives des performances et de l’efficacité énergétique, intégrées dans le noyau Linux depuis la version 5.5. En complément, j’ai proposé un nouveau langage dédié (DSL) pour l’ordonnancement, accompagné de techniques formelles de preuve garantissant l’absence de certains types de bugs dans les algorithmes d’ordonnancement.

 

Ce manuscrit conclut sur mon projet de recherche qui vise à concevoir et certifier des systèmes capables d’exploiter efficacement les serveurs modernes et futurs. Les systèmes actuels utilisent de plus en plus des accès mémoire concurrents non sécurisés pour maximiser les performances matérielles. Cependant, cette approche introduit des complexités importantes, notamment en raison de la diversité croissante du matériel (cœurs hétérogènes, mémoires persistantes, architectures NUMA, accélérateurs). Mon objectif est de surmonter ces défis en concevant des applications capables d’exploiter efficacement ces infrastructures tout en garantissant leur correction par le biais de méthodes formelles.