Models for Storage in Database Backends
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913269873115136 |
|---|---|
| author | Schiebelbein, Edgard Hatia, Saalik Bieniusa, Annette Petri, Gustavo Ferreira, Carla Shapiro, Marc |
| author_facet | Schiebelbein, Edgard Hatia, Saalik Bieniusa, Annette Petri, Gustavo Ferreira, Carla Shapiro, Marc |
| contents | 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 one is a map-based, classical versioned key-value store; the second one, 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 form the basis for a formalisation of a full-fledged backend store with features such as caching or write-ahead logging, as variations on maps and journals. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2403_11716 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Models for Storage in Database Backends Schiebelbein, Edgard Hatia, Saalik Bieniusa, Annette Petri, Gustavo Ferreira, Carla Shapiro, Marc Databases 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 one is a map-based, classical versioned key-value store; the second one, 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 form the basis for a formalisation of a full-fledged backend store with features such as caching or write-ahead logging, as variations on maps and journals. |
| title | Models for Storage in Database Backends |
| topic | Databases |
| url | https://arxiv.org/abs/2403.11716 |