# Models for Storage in Database Backends

## A Rigorous Approach for Formally-Correct Designs

Edgard Schiebelbein

University of Kaiserslautern-Landau
Kaiserslautern, Germany
e_schiebel19@cs.uni-kl.de

Gustavo Petri*

Amazon Web Services
Cambridge, United Kingdom
gfpetri@amazon.co.uk

Saalik Hatia

Sorbonne-Université (LIP6)
Paris, France
saalik.hatia@lip6.fr

Carla Ferreira

Universidade NOVA de Lisboa
Lisbon, Portugal
carla.ferreira@fct.unl.pt

Annette Bieniusa

University of Kaiserslautern-Landau
Kaiserslautern, Germany
bieniusa@cs.uni-kl.de

Marc Shapiro

Sorbonne-Université (LIP6) & Inria
Paris, France
marc.shapiro@acm.org

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

**CCS Concepts: • Theory of computation → Operational semantics; • Information systems → Information storage systems.**

**Keywords:** formal methods, verification, key-value store

## ACM Reference Format:

Edgard Schiebelbein, Saalik Hatia, Annette Bieniusa, Gustavo Petri, Carla Ferreira, and Marc Shapiro. 2024. Models for Storage in Database Backends: A Rigorous Approach for Formally-Correct Designs.

In *The 11th Workshop on Principles and Practice of Consistency for Distributed Data (PaPoC '24), April 22, 2024, Athens, Greece*. ACM, New York, NY, USA, 9 pages. https://doi.org/10.1145/3642976.3653036

## 1 Introduction

A database system manages a collection of digital data. An essential component is the *backend*, which is in charge of recording the data into some memory or *store*. Although conceptually simple at a high level, actual backends are complex, due to the demands for fast response, high volume, limited footprint, concurrency, distribution, and reliability. For instance, the open-source RocksDB comprises 350+ kLOC and Redis is approximately 200 kLOC [5, 11]. Any such complex software has bugs; and database backend bugs are critical, possibly violating data integrity or security [7, 8].

Formal methods have the potential to avoid such bugs, but, given the complexity of a modern backend, fully specifying all the moving pieces is a daunting task.

This paper reports on an incremental approach to the rigorous and modular development of such a backend towards an implementation. To this end, we formalise the semantics of atomic transactions above a versioned key-value store; this high-level specification helps to reason about correctness, both informally and formally with the Coq proof tool. Although this paper focuses on a highly-available transaction model (convergent causal consistency or TCC+, a variant of PSI [13]), our results generalise to stronger models such as SI or strong serialisability. The transaction model appeals to a store's specialised book-keeping operations (called doBegin doUpdate, doCommit, and lookup), implicity assuming infinite memory and no failures.

Next, we instantiate these semantics with two models of the store. The first variant is a classical map-based, versioned key-value store. As a transaction executes, it *eagerly* computes new versions, which it copies into a map upon commit, labelled with the transaction's commit timestamp; reading

<footnote>*This work was conducted while Gustavo Petri was at ARM Ltd.</footnote>

<footnote>Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org. PaPoC '24, April 22, 2024, Athens, Greece</footnote>

<footnote>© 2024 Copyright held by the owner/author(s). Publication rights licensed to ACM.</footnote>

<footnote>ACM ISBN 979-8-4007-0544-1/24/04
https://doi.org/10.1145/3642976.3653036</footnote>
<figure><img src="image_1.png" /><figcaption>Figure 1. Store interface.</figcaption></figure>

a key searches the map for the most recent corresponding version. We plan to mechanise the proof that the map-based model satisfies the transactional specification, i.e., that in any reachable state, a call to read returns the value expected by the semantics for any key and timestamp pair.

Our second variant uses a journal (or log). A transaction
appends individual effects to the journal, tagged with the
transaction identifier; committing appends a commit record,
sealing it with its commit timestamp. Reading from the jour-
nal applies all the relevant effects previously recorded in
the journal. Again, we plan to prove mechanically that the
journal-based store satisfies the abstract specification.

In this paper, we summarize our work-in-progress on
the formal models for the journal- and map-based store. We
define a common interface and show how these stores can
be employed in a transactional storage system. Further, we
sketch their implementation and reasoning about their cor-
rectness in Coq.

The models presented here lack fault-tolerance and es-
sential features such as sharding, caching, write-ahead log-
ging, etc., which are required for state-of-the-art perfor-
mance. Our hypothesis for future work is that such features
can be described and implemented by *composing* instances
of these basic variants.

## 2 System Model and Terminology

Next, we present an informal, high-level overview of the sys-
tem model and terminology. Table 1 overviews our notation.

**Stores and transactions.** At the core of the model is an abstract mutable shared memory, called a *store*, $\sigma \in \Sigma$. A store follows the common API shown in Figure 1. Method lookup returns the value that store $\sigma$ associates with key $k$ at time $t$; an absent mapping returns $\perp$ (i.e., initially, every key maps to $\perp$). Update method `doUpdate` applies a new effect $\delta$ to that key's entry in the store, in order to update the value (see below). Successfully invoking `doCommit` makes the updates of the current transaction visible with a commit timestamp noted `ct`.

Updating a key $k$ under timestamp $t$ creates a new version mapped at index $(k, t)$. A mapping is write-once, and remains valid until the next mapping, if any. For example, suppose store $\sigma$ updates a version of key $k$ at time $t = 100$

with an assignment of 27.<fnref n="1" /> Then, lookup($\sigma$, $k$, 101) should
return 27. If there are no other versions between 100 and 110,
lookup($\sigma$, $k$, 111) should also return 27. If the next mapping
is at timestamp 120, to incr10, then lookup($\sigma$, $k$, 121) should
return 37.

A client (left unspecified by our model) accesses the store
in the context of a *transaction*, a sequence of begin, lookup,
update and commit/abort actions. A transaction reads from a
consistent snapshot of the store, and makes its effects visible
in the store by committing the transaction atomically (all-or-
nothing). We defer a more detailed discussion of transactions
to Section 3.

**Keys, values and timestamps.** Keys, values, and timestamps are opaque types. Keys compare for equality only. Timestamps are partially ordered by $\le$; we say timestamps are *concurrent*, if they are not ordered, i.e., $t_1 \parallel t_2 \stackrel{\text{def}}{=} t_1 \not\le t_2 \land t_2 \not\le t_1$. Note that we do not assume a global clock.

An ordered timestamp pair (OTSP) is of the form $(d, v) \in \mathit{Timestamp} \times \mathit{Timestamp}$, where $d \le v$, called dependence and version respectively. We define a strict partial order relation $<_{\mathit{OTSP}}$ over OTSPs, as follows: $(d_1, v_1) <_{\mathit{OTSP}} (d_2, v_2) \stackrel{\text{def}}{=} v_1 < d_2$. Two OTSPs are concurrent if they cannot be ordered by $<_{\mathit{OTSP}}$:

$$
\begin{align*}
(d_1, v_1) \parallel_{\mathit{OTSP}} (d_2, v_2) \\
\stackrel{\text{def}}{=} (d_1, v_1) \not\le_{\mathit{OTSP}} (d_2, v_2) \land (d_2, v_2) \not\le_{\mathit{OTSP}} (d_1, v_1) \\
\equiv (d_2 \le v_1 \lor d_2 \parallel v_1) \land (d_1 \le v_2 \lor d_1 \parallel v_2)
\end{align*}
$$

**Effects.** Classically, an update simply assigns a new value to the key, as in $k := 27$. Such an assignment creates a new version of $k$ with value 27.

Many recent stores [2, 3, 12] support a more general
concept of update, which we call *effect*. Applying effect $\delta$ to
a current value $v$ computes a new value $\delta(v)$. For instance,
$\delta_{\text{incr10}}$ is the effect that adds 10 to some value. An assignment
is thus a constant effect; for example, $\delta_{\text{assign27}}(v)$ yields 27
whatever the current value $v$.

If a sequence of updates with effects $\delta, \delta', \dots, \delta''$ has
been applied to key $k$, then a store is expected to return value
$(\delta \odot \delta' \odot \dots \odot \delta'')(\perp)$ when queried.<fnref n="2" /> We say a sequence of
effects is *proper* if it starts with an assignment and therefore
evaluates to a value, or $\perp$, when applied to $\perp$; i.e., it does
not depend on any preceding effects. We assume that every
history forms a proper sequence.

An assignment masks any previous effects to the same
key: $\forall \delta, (\delta \odot \delta'_{\text{assign}}) = \delta_{\text{assign}}$; therefore effects that precede

<footnote n="1">¹Assuming integer timestamps, for the sake of example.</footnote>

<footnote n="2">²Operator ⊙ is pronounced “apply;” it is equivalent to classical functional composition o, but associates left to right for convenience: δ ⊙ δ' = δ' ⊙ δ. Note that ⊙ is associative.</footnote>
<table><caption>**Table 1.** Overview of notation.</caption><tr><td>k, t, v</td><td>∈ Key, ∈ Timestamp, ∈ Value</td><td>key, timestamp, value</td></tr><tr><td>δ</td><td>∈ Effect = Value<sub>⊥</sub> → Value</td><td>effect</td></tr><tr><td>⊥</td><td>∈ Effect</td><td>absence of effect</td></tr><tr><td>∘</td><td>∈ Effect<sub>⊥</sub> × Effect<sub>⊥</sub> → Effect<sub>⊥</sub></td><td>effect composition</td></tr><tr><td>x</td><td>∈ X</td><td>Transaction</td></tr><tr><td>τ</td><td>∈ TxnID</td><td>transaction identifier</td></tr><tr><td>st</td><td>∈ Timestamp</td><td>snapshot timestamp (of transaction)</td></tr><tr><td>R</td><td>∈ P(Key)</td><td>read set, keys read in transaction</td></tr><tr><td>W</td><td>∈ P(Key)</td><td>write/dirty set, keys modified in txn</td></tr><tr><td>B</td><td>∈ EffectBuf = Key → Effect<sub>⊥</sub></td><td>effect buffer (of transaction)</td></tr><tr><td>ct</td><td>∈ Timestamp</td><td>commit timestamp (of transaction)</td></tr><tr><td>(τ, st, R, W, B, ct)</td><td>∈ TxnDesc</td><td>transaction descriptor</td></tr><tr><td>X<sub>a</sub>, X<sub>c</sub>, X<sub>r</sub></td><td>⊆ TxnDesc</td><td>aborted, committed, running transactions</td></tr></table>

<table><caption>**Figure 2.** Effect composition.</caption><tr><td>(⊥ ⊙ δ) = (δ ⊙ ⊥) = δ</td><td>(non-effect)</td></tr><tr><td>(δ ⊙ δ') ⊙ δ'' = δ ⊙ (δ' ⊙ δ'')</td><td>(associativity)</td></tr><tr><td>(λv.c) ⊙ δ = λv.δ(c)</td><td>(compacting a proper sequence)</td></tr></table>

the last assignment in a sequence can be safely ignored. Conversely, any proper sequence is equivalent to a single assignment. For instance, $δ_{assign_{27}} ⊙ δ_{incr10} = δ_{assign_{37}}$. This justifies checkpointing a proper sequence into a single assignment. Figure 2 summarizes the rules of effect composition.

**Visibility and concurrent effects.** Effects are ordered by the visibility relation $δ < δ'$ (read “$δ$ is visible to $δ'$”), defined as follows:

* $δ < δ'$ if both belong to the same transaction, and $δ$ is before $δ'$.

* $δ < δ'$ if they belong to different transactions, $x$ and $x'$ respectively, where $x$ has committed, and $x$ is before $x'$ in OTSP order, i.e., $x.ct < x'.st$.

Visibility is a strict partial order. Two effects are concurrent if they are not mutually ordered by visibility.

Some data types support concurrent effects thanks to a merge operator on effects. To ensure convergence, the merge operator is required to be commutative, associative, and idempotent (CAI) [12].

In the presence of concurrent effects, the value expected of key $k$ is results from applying, from the initial $⊥$, the visible effects related to $k$, in visibility order, while merging concurrent effects.

**Concurrent data types.** As an aside, note that classical sequential data types generally disallow concurrent updates, leaving merge undefined. These data types require a strong consistency model, where updates occur in some serial order.

Data types that merge concurrent effects do exist [12]. There are also data types designed with non-assignment effects [1].

To provide the CAI properties, the implementation of an effect typically needs to carry metadata, e.g., to provide idempotence or determine causal relationships between updates. For example, the classical last-writer-wins approach supports concurrency by merging concurrent assignments under some deterministic total order (e.g., timestamp order), and retaining only the one with the highest timestamp. Another example is a counter supporting concurrent increment and decrement effects, which uses a vector of sets of effects, with one entry per (concurrent) client [12]. This representation ensures that a given increment or decrement is applied only once.

## 3 Semantics of Transactions

A transaction $x ∈ X$ is a sequence of effects. We associate to a transaction its *transaction descriptor* $(τ, st, R, W, B, ct)$. It reads from a snapshot timestamped by *snapshot timestamp* st. Its *write buffer* $W$ lists the keys that it *dirtied*, i.e., modified. It may commit with a *commit timestamp* noted ct.

However, the effects of a running transaction are not visible from outside (*isolation*). Within a transaction, an effect *visible* to another one that executes after it (the “read-your-own-writes” property [15]). The semantics formalise this by staging effects to an *effect buffer* $B$. A transaction terminates in an all-or-nothing manner, by either an *abort* that discards its effect buffer, or by a *commit* that makes all its effects visible to later transactions at once. *Atomicity* is formalised by assigning the same, unique, *commit timestamp* to all its effects. The *commit timestamp* of a running or aborted transaction is irrelevant and can be arbitrary, marked by _.

Every first read of some key comes from a same *snapshot*, identified by its *snapshot timestamp* noted st. Transactions that are *visible* in the snapshot are those that committed strictly before its snapshot timestamp.

For interested readers, we provide a small-step operation semantics of transactions in the Appendix in Figure 6.
(a) History.

$\tau_0$: beginTxn(0) · $\tau_0$: update(a, assign$_0$) · $\tau_0$: commit($\tau_0$, 1) · $\tau_1$: beginTxn(2) · $\tau_1$: update(a, incr$_1$) · $\tau_2$: beginTxn(2)
· $\tau_2$: update(a, incr$_2$) · $\tau_1$: commit($\tau_1$, 4) · $\tau_3$: beginTxn(5) · $\tau_2$: commit($\tau_2$, 5) · $\tau_3$: update(a, incr$_4$)
· $\tau_4$: beginTxn(7) · $\tau_3$: commit($\tau_3$, 8) · $\tau_4$: update(a, incr$_8$) · $\tau_4$: commit($\tau_4$, 9)

(b) Dependency graph.

<figure><img src="image_2.png" /></figure>

(c) Map store for key a at t = 11.

(d) Journal store at t = 11.

$$
\sigma[a, t] =
\begin{cases}
(0, \text{assign}_0) & \text{for } t = 1 \\
(2, \text{assign}_1) & \text{for } t = 4 \\
(2, \text{assign}_2) & \text{for } t = 6 \\
(5, \text{assign}_5) & \text{for } t = 8 \\
(7, \text{assign}_{11}) & \text{for } t = 9 \\
\perp & \text{otherwise}
\end{cases}
\qquad
\sigma =
\begin{cases}
\text{(beginTxn, } \tau_0, 0) \triangleright \text{(update, } \tau_0, a, \text{ assign}_0) \triangleright \text{(commit, } \tau_0, 1) \\
\triangleright \text{(beginTxn, } \tau_1, 2) \triangleright \text{(update, } \tau_1, a, \text{ incr}_1) \triangleright \text{(beginTxn, } \tau_2, 2) \\
\triangleright \text{(update, } \tau_2, a, \text{ incr}_2) \triangleright \text{(commit, } \tau_1, 4) \\
\triangleright \text{(beginTxn, } \tau_3, 5) \triangleright \text{(commit, } \tau_2, 5) \triangleright \text{(update, } \tau_3, a, \text{ incr}_4) \\
\triangleright \text{(beginTxn, } \tau_4, 9) \triangleright \text{(commit, } \tau_3, 8) \triangleright \text{(update, } \tau_4, a, \text{ incr}_8) \\
\triangleright \text{(commit, } \tau_4, 9)
\end{cases}
$$

**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 3 illustrates these semantics with an example. The history (Figure 3a) shows a sequence of (atomic) transactional steps; the steps for concurrently executed transactions, like $\tau_1$ and $\tau_2$, are interleaved. For simplicity, the example updates a single key *a* of integer type. Figure 3b visualizes the transactions in a dependency graph.

4 Store Models

This section discusses two basic variants implementing the
general store API. We aim to model their most essential,
primitive properties, abstracting away as much complexity
as possible.

4.1 Map-based store semantics

The *map-based store* models a classic versioned key-value
store as a random-access map, located either in memory or
on disk. It is restricted to contain only values, which (in our
model) are represented as assignment effects. Versions of a
key are distinguished by their version timestamps. Such a
store maps a (*key*, *version timestamp*) pair, to an (*assignment
effect*, *dependency timestamp*) pair.

Figure 4 summarises its semantics. A map store defers its
updates to commit time, and committing atomically copies

the transaction's *effect buffer* into a new version of the cor-
responding keys. lookup searches for the most recent assign
effect directly from the map; both doBegin and doUpdate
are no-ops. Figure 3c illustrates the contents of a map store,
after the history in Figure 3a.

In more detail, mapping $\sigma[k, v] = (d, \delta)$ associates a
versioned key $(k, v)$ with a dependent effect $(d, \delta)$. Here, $v$ is a
version timestamp, $\delta$ is an assignment (a map store does not
support non-assignment effects) associated with metadata $d$, called dependence timestamp, where $d \le v$. Versions are
ordered by their OTSPs $(d, v)$, i.e.,

$$
\sigma[k, v_1] <_{MS} \sigma[k, v_2] \stackrel{\text{def}}{=} v_1 < \sigma[k, v_2].d
$$

When a transaction commits, method doCommit of a
map store eagerly creates a new version for each key modi-
fied by the transaction. The version identifier is the transac-
tion's commit timestamp ct, and it is associated with meta-
data st, the transaction's snapshot timestamp. It returns a
store unchanged except for the new versions.<fnref n="3" />

The versions of *k* visible from the current transaction
are the set $V = \{\sigma[k, v] | v < t\}$. Since a map contains only

<footnote n="3">³A simpler specification might copy all keys, not just the *dirty* ones. However, this is not well-defined when the space of keys is unbounded (e.g., if keys are arbitrary strings).</footnote>
$$
\begin{align*}
\sigma \in (\text{Key} \times \text{Timestamp} \rightarrow \text{Timestamp} \times \text{Assign}) \\
\text{doBegin}(\sigma, \_, \_) &= \sigma \\
\text{lookup}(\sigma, k, t) &= \text{merge}(\max_{<_{\text{MS}}}(\{\sigma[k, v] | v < t\})) \\
\text{doUpdate}(\sigma, \_, \_, \_) &= \sigma \\
\text{doCommit}(\sigma, \_, \text{st}, \_, \mathcal{W}, \mathcal{B}, \text{ct})[k, t] &= \begin{cases} (\text{st}, \mathcal{B}[k]) & \text{if } k \in \mathcal{W} \land t = \text{ct} \\ \sigma[k, t] & \text{otherwise} \end{cases}
\end{align*}
$$

<caption>**Figure 4.** Semantics of map-based store.</caption>

assignments, lookup(σ, k, t) can omit all but the most recent one in this set in visibility order, noted max<sub>MS</sub>(V). To determine the returned value, any concurrent effects are merged (as explained in Section 2), and the resulting assignment effect is then applied to ⊥ to obtain a value.

The map store defers updates to commit time; therefore
doUpdate leaves the store unchanged.

In practice, many existing database backends contain
an in-memory map store, for simplicity and fast reads. To
persist a map store, it suffices to write it to disk periodically;
however such a large write can be slow and is not natively
crash-atomic.

## 4.2 Journal-based store semantics

An alternative store variant is the journal-based store, which logs its updates incrementally to a sequential file.<fnref n="4" /> This design is optimised for fast disk writes, and has good crash-tolerance properties. It is also friendly to non-assignment effects. However, to lookup the value of a key can be slow, as its semantics is to read the journal and applies effects sequentially.

Figure 5 gives the formal semantics of a journal store. A journal store is a finite sequence $\sigma = [e_1, e_2, \dots]$ of records of type BeginTxnRec, update and commit, initially empty. Function doBegin appends a record with transaction identifier $\tau$ and snapshot timestamp st. doUpdate appends an update record that contains transaction identifier $\tau$, key $k$, and effect $\delta$. Similarly, doCommit appends a commit record containing the transaction identifier $\tau$, snapshot timestamp st and commit timestamp ct.

The real action is in lookup(σ, k, t), which accumulates
the effects to key k that committed strictly before t. To for-
malise the procedure is somewhat complex.

* Procedure poststate<sub>σ</sub>(r, k) computes the state of key k after a record r in journal σ takes effect. Records take effect in <<sub>JS</sub> order.

* In <<sub>JS</sub> order, a record of type beginTxn has any num-
  ber of immediate predecessors; other types of records
  have a single one.

* The poststate of an update record with key k and effect $\delta$ is computed by taking the poststate of its immediately-preceding record, and applying $\delta$.

* The poststate of a beginTxn is the merge of poststate of its immediate predecessors.

* Otherwise, the poststate is the same as that of the immediate predecessor; i.e., updates for other keys are ignored, as well as commit records.

Note that a poststate can be computed in a single left-to-
right pass over the journal, because a commit record always
appears before the beginTxn of a transaction that depends
on it. Note also that records are single-assigned and that
poststate<sub>σ</sub> is a function; therefore a practical implementation
may use a cache.

Figure 3d illustrates the contents of a journal store after
execution of the history in Figure 3a. To obtain the value for
lookup(σ, x, 11), we calculate recursively the poststate<sub>σ</sub>s for
τ<sub>3</sub> and τ<sub>4</sub> and merge the results:

$$
\begin{align*}
\text{lookup}(\sigma, a, 11) &= \text{assign}_0 \odot \text{merge}(\{\{\text{incr}_5, \text{incr}_{11}\}\}) \\
&= \text{assign}_{15}
\end{align*}
$$

As explained earlier (Section 2) the implementation of
effects must ensure that the incr₁ from τ₁ executes once only
in the merged value, even though the history contains two
paths to lookup.

5 Formal model in Coq

So far, we have formalized a major part of the definitions
presented in Section 2, 4 and 3 in the proof assistant Coq
with the goal to formally verify their correctness. Our Coq
codebase comprises currently around 2k LOC, without us-
ing any external libraries other than the standard library.
Our goal will be to show that all store variants yield the
expected values under the respective isolation model using
bisimulation.

There are several reasons for choosing to use interactive
theorem proving. A positive aspect about the Coq formaliza-
tion is the high level of abstraction. We can define constructs
with desired properties without the need to provide a specific
implementation. This is in contrast to traditional program-
ming languages, where interfaces or abstract classes can be
defined, but it is usually not possible to restrict the behavior

<footnote n="4">⁴This describes a redo log; an “undo log” would store inverse effects instead.</footnote>
## References

[1] Paulo Sérgio Almeida, Ali Shoker, and Carlos Baquero. 2018. Delta state replicated data types. *Journal of Parallel and Dist. Comp.* 111 (Jan. 2018), 162–173. https://doi.org/10.1016/j.jpdc.2017.08.003

[2] Carlos Baquero, Paulo Sérgio Almeida, and Ali Shoker. 2017. *Pure Operation-Based Replicated Data Types*. ArXiv e-print 1710.04469. arXiv Computing Research Repository (CoRR). http://arxiv.org/abs/1710.04469

[3] Dominic Betts, Julian Dominguez, Grigori Melnik, Fernando Simon-azzi, and Mani Subramanian. 2013. *Exploring CQRS and Event Sourc-ing: A journey into high scalability, availability, and maintainabil-ity with Windows Azure*. Microsoft Patterns & Practices. https://www.microsoft.com/en-us/download/details.aspx?id=34774

[4] Yun-Sheng Chang, Ralf Jung, Upamanyu Sharma, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich. 2023. Verifying vMVCC, a high-performance transaction library using multi-version concurrency control. In *17th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2023, Boston, MA, USA, July 10-12, 2023*, Roxana Geambasu and Ed Nightingale (Eds.). USENIX Association, 871–886. https://www.usenix.org/conference/osdi23/presentation/chang

[5] Facebook. Year of Access. RocksDB. https://github.com/facebook/rocksdb.

[6] Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael Lowell Roberts, Srinath T. V. Setty, and Brian Zill. 2017. IronFleet: proving safety and liveness of practical distributed systems. *Commun. ACM* 60, 7 (2017), 83–92. https://doi.org/10.1145/3068608

[7] Huachao Huang. 2017. How We Found a Data Corruption Bug in RocksDB. Blog post. https://www.pingcap.com/blog/how-to-find-a-rocksdb-bug/.

[8] Kyle Kingsbury and Kit Patella. 2023. Jepsen reports. Blog post. https://jepsen.io/analyses/.

[9] Leslie Lamport. 1994. The Temporal Logic of Actions. *ACM Trans. Program. Lang. Syst.* 16, 3 (1994), 872–923. https://doi.org/10.1145/177492.177726

[10] Pierre Letouzey. 2008. Extraction in Coq: An Overview. In *Logic and Theory of Algorithms, 4th Conference on Computability in Europe, CiE 2008, Athens, Greece, June 15-20, 2008, Proceedings (Lecture Notes in Computer Science, Vol. 5028)*, Arnold Beckmann, Costas Dimitracopoulos, and Benedikt Löwe (Eds.). Springer, 359–369. https://doi.org/10.1007/978-3-540-69407-6_39

[11] Redis. 2024. Redis. https://github.com/redis/redis.

[12] Marc Shapiro, Nuno Preguiça, Carlos Baquero, and Marek Zawirski. 2011. Conflict-free Replicated Data Types. In *Int. Symp. on Stabilization, Safety, and Security of Dist. Sys. (SSS) (Lecture Notes in Comp. Sc. (LNCS), Vol. 6976)*, Xavier Défago, Franck Petit, and V. Villain (Eds.). Springer-Verlag, Grenoble, France, 386–400. https://doi.org/10.1007/978-3-642-24550-3_29

[13] Yair Sovran, Russell Power, Marcos K. Aguilera, and Jinyang Li. 2011. Transactional storage for geo-replicated systems. In *Symp. on Op. Systems Principles (SOSP)*. Assoc. for Computing Machinery, Cascais, Portugal, 385–400. https://doi.org/10.1145/2043556.2043592

[14] Akira Tanaka, Reynald Affeldt, and Jacques Garrigue. 2018. Safe Low-level Code Generation in Coq Using Monomorphization and Monadification. *J. Inf. Process.* 26 (2018), 54–72. https://doi.org/10.2197/IPSJJIP.26.54

[15] Douglas B. Terry, Alan J. Demers, Karin Petersen, Mike J. Spreitzer, Marvin M. Theimer, and Brent B. Welch. 1994. Session Guarantees for Weakly Consistent Replicated Data. In *Int. Conf. on Para. and Dist. Info. Sys. (PDIS)*. IEEE Computer Society, Austin, Texas, USA, 140–149.

[16] James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas E. Anderson. 2015. Verdi: a framework for implementing and formally verifying distributed systems. In *Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015*, David Grove and Stephen M. Blackburn (Eds.). ACM, 357–368. https://doi.org/10.1145/2737924.2737958

## A Formal semantics of transactions

Figure 6 shows the transition rules for the small-step operational semantics of a transaction system build on a store. The specification is fully formal and unambiguous: we find it invaluable to reason about the system, and it is easily translated to the language of a proof tool such as Coq. Most interestingly, it can be read as pseudocode, as we explain now.

The semantics are written as a set of rules. Each rule represents an indivisible state transition; i.e., there are no intermediate states from a semantic perspective, and any intermediate states in the implementation must not be observable.

The system state is represented as a tuple $(\sigma, \mathcal{X}_a, \mathcal{X}_c, \mathcal{X}_r)$ consisting of a store, its field, and the sets of aborted, committed, and running transactions' descriptors.

A rule consists of a set of premises above a long horizontal line, and a conclusion below. A premise is a logical predicate referring to state variables. A variable without a prime mark refers to before the state before the transition (pre-state); a primed variable refers to state after the transition (post-state). Thus a premise that uses only non-primed variables is a pre-condition on the pre-state; if it contains a primed variable, it is a post-condition that constrains the post-state.

If the premises are satisfied, the state-change transition described by the conclusion can take place. A label on the transition arrow under the line represents a client API call. Thus, a rule can be seen as terse pseudocode for the computation to be carried out by the API.

### A.1 Example

To explain the syntax, consider for example rule `BEGINTxN`. The conclusion describes the transition made by API command `beginTxn(st)` from pre-state $(\sigma, \mathcal{X}_a, \mathcal{X}_c, \mathcal{X}_r)$ on the left of the arrow $\begin{array}{c} \text{beginTxn(st)} \\ \xrightarrow{\tau} \end{array}$, to post-state $(\sigma', \mathcal{X}_a, \mathcal{X}_c, \mathcal{X}'_r)$ on the right. Note that in the right-hand side of this conclusion, only $\mathcal{X}_r$ is primed, indicating that the other elements of the state do not change.

### A.2 Parameters

The rules describe a transaction system, which is a tuple $(\sigma, \mathcal{X}_a, \mathcal{X}_c, \mathcal{X}_r)$ consisting of a store $\sigma$, its associated field $\mathcal{F}$, and sets of transaction descriptors $\mathcal{X}_a, \mathcal{X}_c$, and $\mathcal{X}'_r$, which keep track of aborted, committed and running (ongoing) transactions respectively. A transaction descriptor is a tuple $(\tau, st, \mathcal{R}, \mathcal{W}, \mathcal{B}, ct)$ of transaction identifier $\tau$, its snapshot
<figure><img src="image_3.png" /><figcaption>**Figure 6.** Operational semantics of transactions. $\cup$ denotes disjoint set union.</figcaption></figure>

timestamp st, its read set $\mathcal{R}$, its write set $\mathcal{W}$, its effect buffer $\mathcal{B}$, and its commit timestamp ct.<fnref n="5" />

The two timestamps define visibility between transactions, as defined previously (Section 2). Initially, after rule `BEGINTxN`, the sets and the effect buffer are empty and the commit timestamp is invalid. For each key that is accessed, rule `INITKEY` initialises the buffer, and rule `UPDATE` updates it. Computation of the actual commit timestamp may be deferred to the `COMMIT` rule.

The semantic rules are parameterised by commands lookup, `doUpdate`, and `doCommit`, specified in Figure 1. These commands are specialised for each specific store variant: the map-based variant in Section 4.1, the journal-based variant in Section 4.2.

### A.3 Transaction begin

We now consider each rule in turn.

`BEGINTxN` describes how API `beginTxn()` begins a new transaction with snapshot timestamp `st`. The snapshot of the new transaction is timestamped by `st`, passed as an argument; remember that a snapshot includes all transactions that committed with a strictly lesser commit timestamp.

The first premise chooses a fresh transaction identifier $\tau$. The last premise ensures that the appropriate transaction descriptor is in the post-state set of running transactions.

As the transition is labeled by $\tau$, multiple instances of `BEGINTxN` are mutually independent and might execute in parallel, as long as each such transition appears atomic.

### A.4 Reads and writes

Reading or updating operate on the transaction's effect buffer $\mathcal{B}$, which must contain the relevant key.

Rule `INITKEY` specifies a *buffer miss*, which initialises the buffer for some key $k$. As it does not have an API label, it can be called arbitrarily. It modifies only the current transaction's descriptor. Its first premise takes the descriptor of the current transaction $\tau$ from the set of running transactions $X_r$. The second one checks that $k$ is not already in the read set, ensuring that the effect buffer is initialised once per key. The third reads the store by using lookup (specific to a store variant). Next, a premise updates the read set, and another initialises the effect buffer with the return value of lookup. The final premise puts the transaction descriptor, containing the updated read set and effect buffer, back into the descriptor set of running transactions.

In Rule `READ`, API `read(k)` returns a value from the effect buffer. It does not modify the store. The first premise is as above. The second one requires that the key is in the read set.

<footnote n="5">⁵To simplify notation, we may write $\tau.st$ or $\tau.ct$, for instance, for the corresponding elements of the descriptor whose transaction identifier is $\tau$.</footnote>
set, thus ensuring that INITKEY has been applied. The next two premises extract k's mapping from the effect buffer and compute the corresponding return value.

Note the clause $\delta \in Assign$. It requires that, previously to reading, the application has initialised the store with an assignment to k (possibly followed by other effects; such a sequence resolves to an assignment, by associativity, as explained earlier). Otherwise, lookup would return either $\perp$ (if the key has not been initialised at all) or a non-assignment (if the application has stored only non-assignments). We leave the burden of initialisation to the application to simplify the semantics; logically, it's an axiom.

In Rule UPDATE, API call update(k, δ) applies effect δ to key k. It updates both the store and the transaction descriptor. The first two clauses are similar to READ, and similarly require a buffer miss if the key has not been used before (avoiding blind writes). It updates the effect buffer, ensuring that the transaction will read its own writes, and puts the key in the write set. It calls the variant-specific command doUpdate, discussed later in the context of each variant.

## A.5 Transaction termination

A transaction terminates, either by aborting without changing the store, or by committing, which applies its effects atomically to the store.

Rule ABORT moves the current transaction's descriptor from $X_r$ to $X_a$, marking it as aborted. It does not make any other change.

API call commit($\tau$, ct) takes a commit timestamp argument. It is enabled by rule COMMIT, which modifies the store, the running set, and the committed set. The first premise is as usual. Commit timestamp ct must satisfy the constraints stated in the next three premises: it is unique (it does not

appear in $X_c$); it is greater or equal to the snapshot; the NoInversion(ct) premise ensures that no already-committed or running transaction may depend on this one.

The latter premise aims to protect against the case where another transaction has read a value that this transaction has yet to write, because the transactions commit in the wrong order. To understand, consider the following anomalous example: (i) Transaction $\tau_1$ has commit timestamp 1; (ii) Transaction $\tau_2$ starts with snapshot timestamp 2 > 1; thus $\tau_2$ reads the updates made by $\tau_1$; (iii) however, $\tau_1$ is slow and its committed effects reach the store only after the read by $\tau_2$. Clearly, this would be incorrect. To avoid this issue, $\tau_2$ must not start until $\tau_1$ has finalised its transition to committed. This requires synchronisation between concurrent transactions.

To avoid this issue, no still-running or committed transaction may read from the current transaction, i.e.,

$$ \exists x \in X_c \cup X_r : ct < x.st \land W \cap x.R \neq \emptyset $$

This expression requires to keep track of the read-set of committed transactions; to avoid this, we could check running transactions only, using the slightly stronger expression:

$$ \exists x \in X_c \cup X_r : ct < x.st \land (x \in X_r \Rightarrow W \cap x.R \neq \emptyset) $$

For simplicity, we choose to use the even stronger premise

$$ \text{NoInversion(ct)} \stackrel{\text{def}}{=} \exists x \in X_c \cup X_r : ct < x.st $$

at the cost of aborting transactions unnecessarily.

Operation doCommit (specific to a store variant) provides the new state of the store; it should ensure that the effects of the committed transaction become visible in the store, labelled with the commit timestamp. Finally, the transaction descriptor, now containing the commit timestamp, is moved to the set of committed transactions.