Certified Mergeable Replicated Data Types
(Extended Version)

As an alternative to CRDTs, mergeable replicated data types (MRDTs) (Kaki et al., 2019) have been proposed, which extend the idea of distributed version control for arbitrary data types. The causal context necessary for resolving the conflicts is maintained by the MRDT middleware. MRDTs allow ordinary purely functional data structures (Okasaki, 1999) to be promoted to RDTs by equipping them with a three-way merge function that describes the conflict resolution policy. When conflicting updates need to be reconciled, the causal history is used to determine the lowest common ancestor (lca) for use in the three-way merge function along with the conflicting states. The MRDT middleware garbage collects the causal histories when appropriate (Dubey, 2021), and is no longer a concern for the RDT library developer. This branch-consistent view of replication not only makes it easier to develop individual data types, but also leads to a natural transactional semantics (Crooks et al., 2016; Dubey et al., 2020).

An efficient OR-set MRDT that avoids tombstones can be implemented as follows. We represent the OR-set as a list of pairs of the element and a unique id, which is generated per operation. The list may have duplicate elements with different ids. Adding an element appends the element and the id pair to the head of the list ($O(1)$ operation). Removing an element removes all the occurrences of the element from the list ($O(n)$ operation). Given two concurrent versions of the OR-set $a$ and $b$, and their lowest common ancestor $l$, the merge is implemented as $(a-l)~{}@~{}(b-l)~{}@~{}(l\cap a\cap b)$, where $@$ stands for list append. Intuitively, we append the lists formed by newly added elements in $a$ and $b$ with the list of elements that are present on all the three versions. The unique id associated with the element ensures that in the presence of concurrent addition and removal of the same element, the newly added element with the fresh id, which has not been seen by the concurrent remove, will remain in the merged result. The merge operation can be implemented in $O(n~{}log~{}n)$ time by sorting the individual lists. In §2.1.2, we show how to make this implementation even more efficient by removing the duplicate elements with different ids from the OR-set.

The key question is how do we guarantee that such efficient implementations still preserve the intent of the OR-Set in a sound manner? Optimisations such as removing duplicate elements are notoriously difficult to get right since the replica states evolve independently. Moreover, individually correct RDTs may fail to preserve convergence when put together (Kleppmann, 2020). Kaki et al. (Kaki et al., 2019) opine that merge functions should not be written by hand, but automatically derived from a relational representation of the sequential data type. Their idea is to capture the key properties of the algebraic data type as relations over its constituent elements. Then, the merge function devolves to a merge of these relations (sets) expressed as MRDTs. During merge, the concrete implementations are reified to their relational representations expressed in terms of sets, merged using set semantics, and the final concrete state is reconstructed from the relational set representation.

Unfortunately, mapping complex data types to sets does not lead to efficient implementations. For example, a queue in Kaki et al. is represented by two characteristic relations – a unary relation for membership and a binary relation for ordering. For a queue with $n$ elements, the ordering relation contains $n^{2}$ elements. Reifying the queue to its characteristic relations and back to its concrete representation for every merge is inefficient and impractical. This technique does not scale as the structure of the data type gets richer (Red-Black tree, JSON, file systems, etc.). The more complex the data type, more complex the characteristic relations become, having an impact on the cost of merge. Further Kaki et al. do not consider functional correctness of MRDT implementations, but instead only focuses on the correctness of convergence.

Precisely specifying and verifying the functional correctness of efficient RDT implementations is not straightforward due to the complexity of handling conflicts between divergent versions. This results in a huge gap between the high-level specifications and efficient implementations. In this work, we propose to bridge this gap by using Burckhardt et al.’s replication-aware simulation relation (Burckhardt et al., 2014). However, Burckhardt et al.’s simulation is only applicable to CRDTs and cannot be directly extended to MRDTs which assume a different system model.

We first propose a system model and an operational semantics for MRDTs, and precisely define the problem of convergence and functional correctness for MRDTs. We also introduce a new notion of convergence modulo observable behaviour, which allows replicas to converge to different states, as long as their observable behaviour to clients remains the same. This notion allows us to build and verify even more efficient MRDTs.

Further, we go beyond Burckhardt et al.’s work (Burckhardt et al., 2014) in the use of simulation relations by mechanizing and automating (to an extent) the complete verification process. We instantiate our technique as an F* library named Peepul and mechanically verify the implementation of a number efficient purely functional MRDT implementations including an efficient replicated two-list queue. Our replicated queue supports constant time push and pop operations, a linear time merge operation, and does not have any tombstones. To the best of our knowledge, ours is the first formal declarative specification of a distributed queue (§6), and its mechanised proof of correctness.

Being a SMT-solver-aided programming language, F* allows us to discharge many of the proof obligations automatically through the SMT solver. Even though our approach requires the simulation relation as input, we also observe that in most cases, the simulation relation directly follows from the declarative specification.

Our technique also supports composition, and we demonstrate how parametric polymorphism allows composition of not just the MRDT implementations but also their proofs of correctness. From our MRDT implementations in F*, we extract verified OCaml implementations and execute them on top of Irmin, a Git-like distributed database. Our experimental evaluation shows that our efficient MRDT implementations scale significantly better than other RDT implementations.

To summarize, we make the following contributions:

• •

  We propose a store semantics for MRDT implementations and formally define the convergence and functional correctness problem for MRDTs, including a new notion of convergence modulo observable behaviour.

• •

  We propose a technique to verify both convergence and functional correctness of MRDTs by adapting the notion of replication-aware simulation relation (Burckhardt et al., 2014) to the MRDT setting.

• •

  We mechanize and automate the complete verification process using F*, and apply our technique on a number of complex MRDT implementations, including a new time and space-efficient ORSet and a queue MRDT.

• •

  We provide experimental results which demonstrate that our efficient MRDT implementations perform much better as compared with previous implementations, and also show the tradeoff between proof automation and verification time in F*.

The rest of the paper is organized as follows. §2 presents the implementation model and the declarative specification framework for MRDTs. §3 presents the formal semantics of the git-like replicated store on which MRDT implementations run. In §4, we present a new verification strategy for MRDTs based on the notion of replication-aware simulation. §5 highlights the compositionality of our technique in verifying complex verified MRDTs reusing the proofs of simpler ones. §6 presents the formally verified efficient replicated queue. §7 presents the experimental evaluation and §8 presents the related work.

Our model of replicated datastore is similar to a distributed version control system like Git (Git, 2021), with replication centred around versioned states in branches and explicit merges. A typical replicated datastore will have a key-value interface with the capability to store arbitrary objects as values (Riak, 2021; Irmin, 2021). Since our goal is to verify correct implementations of individual replicated objects, our formalism models a store with a single object.

A replicated datastore consists of an object which is replicated across multiple branches $b_{1},b_{2},\ldots\in branchID$. Clients interact with the store by performing operations on the object at a specified branch, modifying its local state. The different branches may concurrently update their local states and progress independently. We also allow dynamic creation of a new branch by copying the state of an existing branch. A branch at any time can get updates from any other branch by performing a merge with that branch, updating its local copy to reflect the merge. Conflicts might arise when the same object is modified in two or more branches, and these are resolved in an data type specific way.

An object has a type $\tau\in Type$, whose type signature $(Op_{\tau},Val_{\tau})$ determines the set of supported operations $Op_{\tau}$ and the set of their return values $Val_{\tau}$. A special value $\bot\in Val_{\tau}$ is used for operations that return no value.

An MRDT implementation $\mathcal{D_{\tau}}$ provides two methods: do and merge that the datastore will invoke appropriately. We assume that these methods execute atomically. A client request to perform an operation $o\in Op_{\tau}$ at a branch triggers the call $do(o,\sigma,t)$. This takes the current state $\sigma\in\Sigma$ of the object at the branch where the request is issued and a timestamp $t\in Timestamp$ provided by the datastore, and produces the updated object state and the return value of the operation.

The datastore guarantees that the timestamps are unique across all of the branches, and for any two operations $a$ and $b$, with timestamps $t_{a}$ and $t_{b}$, if $a$ happens-before $b$, then $t_{a}<t_{b}$. The data type implementation can use the timestamp provided to implement the conflict-resolution strategy, but is also free to ignore it. For simplicity of presentation, we assume that the timestamps are positive integers, $Timestamp=\mathbb{N}$. The datastore may choose to implement the timestamp using Lamport clocks (Lamport, 1978), along with the unique branch id to provide uniqueness of timestamps.

A branch $a$ may get updates from another branch $b$ by performing a merge, which modifies the state of the object in branch $a$. In this case, the datastore will invoke $merge(\sigma_{lca},\allowbreak\sigma_{a},\allowbreak\sigma_{b})$ where $\sigma_{a}$ and $\sigma_{b}$ are the current states of branch $a$ and $b$ respectively, and $\sigma_{lca}$ is the lowest common ancestor (LCA) of the two branches. The LCA of two branches is the most recent state from which the two branches diverged. We assume that execution of the store will begin with a single branch, from which new branches may be dynamically created. Hence, for any two branches, the LCA will always exist.

Given that there are several candidates for implementing an MRDT, we need a way to specify the behaviour of an MRDT so that we may ask the question of whether the given implementation satisfies the specification. We now present a declarative framework for specifying MRDTs which closely follows the framework presented by Burckhardt et al. (Burckhardt et al., 2014). We define our specifications on an abstract state, which capture the state of the distributed store. It consists of events in a execution of the distributed store, along with a visibility relation among them.

Given $e\xrightarrow{vis}f$, $e$ is said to causally precede $f$. In our setting, it may be the case that the operation of $f$ follows the operation of $e$ on the same branch, or the operations of $f$ and $e$ were performed on different branches $b_{f}$ and $b_{e}$, but before the operation of $f$, the branch $b_{e}$ on which the operation of $e$ was performed was merged info $b_{f}$.

We specify a data type $\tau$ by a function $\mathcal{F_{\tau}}$ which determines the return value of an operation $o$ based on prior operations applied on that object. $\mathcal{F_{\tau}}$ also takes as a parameter the abstract state that is visible to the operation. Note that the abstract state contains all the information that is necessary to specify the return-value of $o$.

For proving the correctness of a data type implementation $\mathcal{D}_{\tau}$, we use replication-aware simulation relations $~{}\mathcal{R}_{sim}$. While similar to the simulation relations used in Burckhardt et al. (Burckhardt et al., 2014), in this work, we apply them to MRDTs rather than CRDTs. Further, we also mechanize and automate simulation-based proofs by deriving simple sufficient conditions which can easily discharged by tools such as F*. Finally, we apply our proof technique on a wide range of MRDTs, with substantially complex specifications (e.g. queue MRDT described in §6).

The $\mathcal{R}_{sim}$ relation essentially associates the concrete state of the object at a branch $b$ with the abstract state at the branch. This abstract state would consist of all events which were applied on the branch. Verifying the correctness of a MRDT through simulation relations involves two steps: (i) first, we show that the simulation relation holds at every transition in every execution of the replicated store, and (ii) the simulation relation meets the requirements of the data type specification and is sufficient for convergence. The first step is essentially an inductive argument, for which we require the simulation relation between the abstract and concrete states to hold for every data type operation instance and merge instance. These two steps are depicted pictorially in figures 4 and 5, respectively.

Figure 4 considers the application of a data type operation (through the $do$ function) at a branch. Assuming that the simulation relation $\mathcal{R}_{sim}$ holds between the abstract state $I$ and the concrete state $\sigma$ at the branch, we would have to show that $\mathcal{R}_{sim}$ continues to hold after the application of the operation through the concrete $do$ function of the implementation and the abstract $do^{\#}$ function on the abstract state.

Figure 5 considers the application of a merge operation between branches $a$ and $b$. In this case, assuming $\mathcal{R}_{sim}$ between the abstract and concrete states at the two branches and for the LCA, we would then show that $\mathcal{R}_{sim}$ continues to hold between the concrete and abstract states obtained after merge. Note that since the concrete merge operation also uses the concrete LCA state $\sigma_{lca}$, we also assume that $\mathcal{R}_{sim}$ holds between the concrete and abstract LCA states.

These conditions consider the effect of concrete and abstract operations locally and thus enable automated verification. In order to discharge these conditions, we also consider two store properties, $\Psi_{ts}$ and $\Psi_{lca}$ that hold across all executions (shown in Table 1). $\Psi_{ts}$ pertains to the nature of the timestamps associated with each operation, while $\Psi_{lca}$ characterizes the lowest common ancestor used for merge. These properties hold naturally due to the semantics of the replicated store. These properties play an important role in discharging the conditions required for validity of the simulation relation.

In particular, $\Psi_{ts}(I)$ asserts that in the abstract state $I$, causally related events have increasing timestamps, and no two events have the same timestamp. $\Psi_{lca}(I_{l},I_{a},I_{b})$ will be instantiated with the LCA of two abstract states $I_{a}$ and $I_{b}$ (i.e. $I_{l}=lca^{\#}(I_{a},I_{b})$), and asserts that the visibility relation between events which are present in both $I_{a}$ and $I_{b}$ (and hence also in $I_{l}$) will be the same in all three abstract states. Further, every event in the LCA will be visible to newly added events in either of the two branches. These properties follow naturally from the definition of LCA and are also maintained by the store semantics.

Table 2 shows the conditions required for proving the validity of the simulation relation $\mathcal{R}_{sim}$. In particular, $\Phi_{do}$ and $\Phi_{merge}$ exactly encode the scenarios depicted in the figures 4 and 5. Note that for $\Phi_{do}$, we assume $\Psi_{ts}$ for the input abstract state on which the operation will be performed. Similarly, for $\Phi_{merge}$, we assume $\Psi_{ts}$ for all events in the merged abstract state (thus ensuring $\Psi_{ts}$ also holds for events in the original branches) and $\Psi_{lca}$ for the LCA of the abstract states.

Once we show that the simulation relation is maintained at every transition in every execution inductively, we also have to show that it is strong enough to imply the data type specification as well as guarantee convergence. For this, we define two more conditions $\Phi_{spec}$ and $\Phi_{con}$ (also in table 2). $\Phi_{spec}$ says that if abstract state $I$ and concrete state $\sigma$ are related by $\mathcal{R}_{sim}$, then the return value of operation $o$ performed on $\sigma$ should match the value of the specification function $\mathcal{F}_{\tau}$ on the abstract state. Since the $\mathcal{R}_{sim}$ relation is maintained at every transition, if $\Phi_{spec}$ is valid, then the implementation will clearly satisfy the specification. Finally, for convergence, we require that if two concrete states are related to the same abstract state, then they should be observationally equivalent. This corresponds to our proposed notion of convergence modulo observable behavior.

Let us look at the simulation relations for verifying OR-set implementations in §2.1 against the specification $\mathcal{F}_{orset}$ in §2.2.1.

To illustrate the benefits of compositionality, we consider a decentralised IRC-like chat application with multiple channels. Each channel maintains the list of messages in reverse chronological order so that the most recent message may be displayed first. For simplicity, we assume that the channels are append-only; while new messages can be posted to the channels, old messages cannot be deleted. We also assume that while new channels may be created, existing channels may not be deleted.

The chat application supports sending a message to a channel and reading messages from a channel: $Op_{chat}=\{send(ch,m)\mid ch\in string\ ~{}\wedge~{}m\in string)\}~{}\cup~{}\{rd(ch)\allowbreak\mid ch\in string\}$. The specification of this chat application is given in Figure 6. For this we define a predicate $ord$ such that $ord(t_{1},m_{1})~{}(t_{2},m_{2})~{}l$ holds iff $t_{1}\neq t_{2}$ and $(t_{1},m_{1})$ occurs before $(t_{2},m_{2})$ in list $l$. The specification essentially says the log of messages contains all (and only those) messages that were sent, and messages are ordered in reverse chronological order.

Rather than implement this chat application from scratch, we may quite reasonably build it using existing MRDTs. We may use a MRDT map to store the association between the channel names and the list of messages. Given that the conversations take place in a decentralized manner, the list of messages in each channel should also be mergeable. For this purpose, we use a mergeable log, an MRDT list that totally orders the messages based on the message timestamp, to store the messages in each of the channels. As mentioned earlier, for simplicity we will assume that the map and the log are grow-only.