Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Models for Storage in Database Backends

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

TL;DR

This paper presents the formalisation of the expected behaviour of a basic transactional system that calls into a simple store API, and instantiate in two semantic models that are a map-based, classical versioned key-value store and a journal-based one.

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 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.

Models for Storage in Database Backends

TL;DR

This paper presents the formalisation of the expected behaviour of a basic transactional system that calls into a simple store API, and instantiate in two semantic models that are a map-based, classical versioned key-value store and a journal-based one.

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 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.
Paper Structure (17 sections, 10 equations, 5 figures, 1 table)

This paper contains 17 sections, 10 equations, 5 figures, 1 table.

Table of Contents

  1. Introduction
  2. System Model and Terminology
  3. Stores and transactions
  4. Keys, values and timestamps
  5. Effects
  6. Visibility and concurrent effects
  7. Concurrent data types
  8. Semantics of Transactions
  9. Store Models
  10. Map-based store semantics
  11. Journal-based store semantics
  12. Formal model in Coq
  13. Discussion and Outlook
  14. Formal semantics of transactions
  15. Example
  16. ...and 2 more sections

Figures (5)

  • Figure 1: Store interface.
  • Figure 2: Effect composition.
  • Figure 3: Example of execution trace. The history (a) shows the order in which the transactional operations are executed. The dependency graph (b) visualizes the partial order of the transactions. The map (c) and journal (d) show the different stores after the history executed.
  • Figure 4: Semantics of map-based store.
  • Figure 5: Semantics of journal-based store.