Models for Storage in Database Backends
<|reference_start|>Models for Storage in Database Backends: 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.<|reference_end|>
@article{schiebelbein2024models,
    title={Models for Storage in Database Backends},
    author={Edgard Schiebelbein, Saalik Hatia, Annette Bieniusa, Gustavo Petri
  (Amazon Web Services), Carla Ferreira (NOVA), Marc Shapiro (DELYS)},
    journal={arXiv preprint arXiv:2403.11716},
    year={2024},
    doi={10.1145/3642976.3653036},
    archivePrefix={arXiv},
    eprint={2403.11716},
    primaryClass={cs.DB}
}