Automatically Verifying Replication-aware Linearizability
Vimala Soundarapandian, Kartik Nagar, Aseem Rastogi, KC Sivaramakrishnan
TL;DR
This work tackles verifying replication-aware linearizability for Mergeable Replicated Data Types (MRDTs) under arbitrary merges by introducing a bottom-up linearization technique. It formalizes MRDT semantics and RA-linearizability, then reduces correctness to proving a small set of inductive verification conditions that can be automatically discharged in the F$^\star$ framework, with code extraction to OCaml. The approach supports MRDTs and state-based CRDTs, demonstrated on a polymorphic JSON MRDT and other datatypes, and even uncovers bugs in prior implementations (e.g., Enable-wins flag) that are resolved by additional per-replica state management. The combination of a formal RA-linearizability model, a constructive no-rc-chain/conditional-commutativity toolkit, and automated VC verification yields scalable, automated proofs of both convergence and functional correctness for complex replicated data types, advancing reliable decentralized storage systems.
Abstract
Data replication is crucial for enabling fault tolerance and uniform low latency in modern decentralized applications. Replicated Data Types (RDTs) have emerged as a principled approach for developing replicated implementations of basic data structures such as counter, flag, set, map, etc. While the correctness of RDTs is generally specified using the notion of strong eventual consistency--which guarantees that replicas that have received the same set of updates would converge to the same state--a more expressive specification which relates the converged state to updates received at a replica would be more beneficial to RDT users. Replication-aware linearizability is one such specification, which requires all replicas to always be in a state which can be obtained by linearizing the updates received at the replica. In this work, we develop a novel fully automated technique for verifying replication-aware linearizability for Mergeable Replicated Data Types (MRDTs). We identify novel algebraic properties for MRDT operations and the merge function which are sufficient for proving an implementation to be linearizable and which go beyond the standard notions of commutativity, associativity, and idempotence. We also develop a novel inductive technique called bottom-up linearization to automatically verify the required algebraic properties. Our technique can be used to verify both MRDTs and state-based CRDTs. We have successfully applied our approach to a number of complex MRDT and CRDT implementations including a novel JSON MRDT.