HATIA Saalik

دكـتور
وحـدة : DELYS
تاريـخ المـغادرة : 02/06/2023
https://lip6.fr/Saalik.Hatia

رئاسـة البـحث : 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.

مناقـشـة مـذكـرة : 01/06/2023

أعـضاء لجنة المناقـشة :

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

تاريـخ المـغادرة : 02/06/2023

إصدارات 2020-2024

Mentions légales
خـريـطـة المـوقـع