Models for Storage in Database Backends

Edgard Schiebelbein, Saalik Hatia, Annette Bieniusa, Carla Ferreira, Gustavo Petri, Marc Shapiro

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

This paper describes ongoing work on developing a formal specification of a database backend. We present the formalisation of the expected behaviour of a basic transactional system that calls into a simple store API, and instantiate in two semantic models. The first is a map-based, classical versioned key-value store; the second, journal-based, appends individual transaction effects to a journal. We formalise a significant part of the specification in the Coq proof assistant. This work will be the basis for formalising a full-fledged backend store with features such as caching or write-Ahead logging as variations on maps and journals.
Original languageEnglish
Title of host publicationPaPoC '24
Subtitle of host publicationProceedings of the 11th Workshop on Principles and Practice of Consistency for Distributed Data
Place of PublicationNew York
PublisherACM - Association for Computing Machinery
Pages58-66
Number of pages9
ISBN (Electronic)979-8-4007-0544-1
DOIs
Publication statusPublished - Apr 2024
Event11th ACM Workshop on Principles and Practice of Consistency for Distributed Data
- Athens, Greece
Duration: 22 Apr 202422 Apr 2024

Publication series

NameEuroSys: European Conference on Computer Systems
PublisherACM - Association for Computing Machinery

Conference

Conference11th ACM Workshop on Principles and Practice of Consistency for Distributed Data
Abbreviated titlePAPOC 2024
Country/TerritoryGreece
CityAthens
Period22/04/2422/04/24

Keywords

  • formal methods
  • key-value store
  • verification

Fingerprint

Dive into the research topics of 'Models for Storage in Database Backends'. Together they form a unique fingerprint.

Cite this