HATIA Saalik

doctorant à Sorbonne Université
Équipe : DELYS
https://lip6.fr/Saalik.Hatia

Direction de recherche : Marc SHAPIRO

Utilisation de spécifications formelle pour implémenter un backend de base de données

Conceptuellement, un système de stockage de base de données est une simple mappe entre clés et valeurs. Cependant, afin d’offrir performances élevées et fiabilité, une base de donnée moderne est un système complexe et concurrent, ce qui rend ouvre la porte aux erreurs.
Cette thèse relate notre parcours, allant de la spécification formelle d’une base de données à sa mise en œuvre. La spécification est courte et non ambigüe, et aide à raisonner sur la justesse. La lecture de la spécification permet de dégager les problèmes importants et tient lieu de pseudocode rigoureux pour la mise en œuvre.
La spécification décrit la couche de stockage comme une mémoire partagée transactionnelle simple, avec deux variantes (au comportement équivalent), basées respectivement sur une mappe et un journal. Nous mettons en œuvre ces deux variantes, en suivant fidèlement notre spécification. Les mécanismes complexes d’une base de données moderne, comme un système de journalisation, tronqué à volonté grâce à des points de reprise, comme une composition des deux variants. Finalement, nous présentons une évaluation expérimentale, avec des performances qui sont acceptables pour une mise en œuvre rigoureuse.

Soutenance : 01/06/2023

Membres du jury :

Emmanuelle Anceaume, Directrice de recherche, IRISA, Université de Rennes-I [Rapporteur]
Gaël Thomas, Professeur, Télécom SudParis [Rapporteur]
Carla Ferreira, Maîtresse de Conférences, Université NOVA de Lisbon
Antoine Miné, Professeur, Sorbonne Université, LIP6
Serdar Tasiran, Principal Applied Scientist, Amazon
Patrick Valduriez, Directeur de recherche, Inria, Université de Montpellier
Marc Shapiro, Directeur de Recherche Emérite, SU, LIP6, Inria
Annette Bieniusa, Professeure, TU Kaiserslautern

Date de départ : 02/06/2023

Publications 2020-2024