Certified Mergeable Replicated Data Types

TL;DR

This paper introduces Peepul, a novel framework for designing and verifying efficient replicated data types (RDTs) by modeling them as version control systems with a three-way merge, ensuring correctness and convergence.

Contribution

Peepul provides a practical methodology and verification approach for building efficient RDTs, bridging correctness with performance in distributed systems.

Findings

Verified RDTs are extracted as OCaml code for practical use.

Peepul's approach ensures convergence and correctness of RDTs.

Implemented in Irmin, a Git-like distributed database.

Abstract

Replicated data types (RDTs) are data structures that permit concurrent modification of multiple, potentially geo-distributed, replicas without coordination between them. RDTs are designed in such a way that conflicting operations are eventually deterministically reconciled ensuring convergence. Constructing correct RDTs remains a difficult endeavour due to the complexity of reasoning about independently evolving states of the replicas. With the focus on the correctness of RDTs (and rightly so), existing approaches to RDTs are less efficient compared to their sequential counterparts in terms of time and space complexity of local operations. This is unfortunate since RDTs are often used in a local-first setting where the local operations far outweigh remote communication. In this paper, we present Peepul, a pragmatic approach to building and verifying efficient RDTs. To make reasoning about correctness easier, we cast RDTs in the mould of a distributed version control system, and equip it with a three-way merge function for reconciling conflicting versions. Further, we go beyond just verifying convergence, and provide a methodology to verify arbitrarily complex specifications. We develop a replication-aware simulation relation to relate RDT specifications to their efficient purely functional implementations. We implement Peepul as an F* library that discharges proof obligations to an SMT solver. The verified efficient RDTs are extracted as OCaml code and used in Irmin, a Git-like distributed database.