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.

Publications 2020-2024

• 2024
  • E. Schiebelbein, S. Hatia, A. Bieniusa, G. Petri, C. Ferreira, M. Shapiro : “Models for Storage in Database Backends: A Rigorous Approach for Formally-Correct Designs”, Proceedings of the EuroSys 2024 workshops, Athènes, Greece (2024)
• 2023
  • S. Hatia : “Leveraging formal specification to implement a database backend”, thèse, soutenance 01/06/2023, direction de recherche Shapiro, Marc (2023)
• 2020
  • S. Hatia, M. Shapiro : “Specification of a Transactionally and Causally-Consistent (TCC) database”, (2020)