Informations professionnelles
Statut: Docteur ED
ED: EDITE
Unité de recherche: LIP6
Employeur: Sorbonne Université Date de debut de thèse: 1 octobre 2018 Date soutenance de thèse: 1 juin 2023 Directeur de thèse: Marc SHAPIRO (LIP6) Sujet de thèse: Efficient management of memory and storage for CRDTs Thématique : Systèmes et réseaux
Employeur: Sorbonne Université Date de debut de thèse: 1 octobre 2018 Date soutenance de thèse: 1 juin 2023 Directeur de thèse: Marc SHAPIRO (LIP6) Sujet de thèse: Efficient management of memory and storage for CRDTs Thématique : Systèmes et réseaux
Soutenance de thèse
Données générales
Titre : Leveraging formal specification to implement a database backend
Date : 1 juin 2023
Heure: 14:00
Résumé : Conceptually, 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.
Lieu : Amphitheatre Astier
Bâtiment Esclangon
4 Place Jussieu,
75005 Paris
Rapporteurs/ Rapporteuses
| Personne | Qualité | Etablissement |
|---|---|---|
| M. Thomas Gaël | Professeur des universités | Services répartis, Architectures, MOdélisation, Validation, Administration des Réseaux |
| Mme. Anceaume Emmanuelle | Directrice de recherche (HDR) | Institut de Recherche en Informatique et Systèmes Aléatoires, Univ. Rennes |
Composition du jury
| Personne | Qualité | Etablissement |
|---|---|---|
| M. Shapiro Marc | Directeur de recherche (HDR) | LIP6, Sorbonne Université |
| M. Thomas Gaël | Professeur des universités | Services répartis, Architectures, MOdélisation, Validation, Administration des Réseaux |
| Mme. Anceaume Emmanuelle | Directrice de recherche (HDR) | Institut de Recherche en Informatique et Systèmes Aléatoires, Univ. Rennes |
| Mme. Ferreira Carla | Maîtresse de Conférences | University of Lisbon (Portugal) |
| M. Serdar Tasiran | Industriel | AMAZON (États-Unis) |
| M. Patrick Valduriez | Directeur de recherche | Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier |
| M. Mine Antoine | Professeur des universités | LIP6, Sorbonne Université |