HATIA Saalik

PhD graduated
Team : DELYS
Departure date : 06/02/2023

Supervision : 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.

Defence : 06/01/2023

Jury members :

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

Departure date : 06/02/2023

2020-2024 Publications