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 language | English |
---|---|
Title of host publication | PaPoC '24 |
Subtitle of host publication | Proceedings of the 11th Workshop on Principles and Practice of Consistency for Distributed Data |
Place of Publication | New York |
Publisher | ACM - Association for Computing Machinery |
Pages | 58-66 |
Number of pages | 9 |
ISBN (Electronic) | 979-8-4007-0544-1 |
DOIs | |
Publication status | Published - Apr 2024 |
Event | 11th ACM Workshop on Principles and Practice of Consistency for Distributed Data - Athens, Greece Duration: 22 Apr 2024 → 22 Apr 2024 |
Publication series
Name | EuroSys: European Conference on Computer Systems |
---|---|
Publisher | ACM - Association for Computing Machinery |
Conference
Conference | 11th ACM Workshop on Principles and Practice of Consistency for Distributed Data |
---|---|
Abbreviated title | PAPOC 2024 |
Country/Territory | Greece |
City | Athens |
Period | 22/04/24 → 22/04/24 |
Keywords
- formal methods
- key-value store
- verification