Effective verification of replicated data types using later appearance records (LAR)

Abstract

Replicated data types store copies of identical data across multiple servers in a distributed system. For the replicas to satisfy strong eventual consistency, these data types should be designed to guarantee conflict free convergence of all copies in the presence of concurrent updates. This requires maintaining history related metadata that, in principle, is unbounded. While earlier work such as [2] and [9] has concentrated on declarative frameworks for formally specifying Conflict-free Replicated Data Types (CRDTs) and conditions that guarantee the existence of finite-state (distributed) reference implementations, there has not been a systematic attempt so far to use the declarative specifications for effective verification of CRDTs. In this work, we propose a simple global reference implementation for CRDTs specified declaratively, and simple conditions under which this is guaranteed to be finite. Our implementation uses the technique of Later Appearance Record (LAR). We also outline a methodology for effective verification of CRDT implementations using CEGAR.