HATIA Saalik

Dottore di ricerca
Gruppo di ricerca : DELYS
Data di partenza : 06/02/2023
https://lip6.fr/Saalik.Hatia

Relatore : Marc SHAPIRO

Leveraging formal specification to implement a database backend

onceptually, a database storage backend is just a map of keys to values. However, to provide performance and reliability, a modern store is a complex, concurrent software system, opening many opportunities for bugs.
This thesis reports on our journey from formal specification of a store to its implementation. The specification is terse and unambiguous, and helps reason about correctness. Read as pseudocode, the specification provides a rigorous grounding for implementation.
The specification describes a store as a simple transactional shared memory, with two (behaviourally equivalent) variants, map- and journal-based.We implement these two basic variants verbatim in Java. We specify the features of a modern store, such as a write-ahead log with checkpointing and truncation, as a dynamic composition of instances of the two basic variants.
Our experimental evaluation of an implementation has acceptable performance, while our rigorous methodology increases confidence in its correctness.

Difesa : 06/01/2023

Membri della commissione :

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

Data di partenza : 06/02/2023

Pubblicazioni 2020-2024

Mentions légales
Mappa del sito