ReDunT: Automatically Deriving Redundancy Relations for Pure Op-Based CRDTs

Conflict-free Replicated Data Types (CRDTs) are a family of data structures that incorporate conflict resolution mechanisms to ensure state convergence and ease the development of highly available distributed systems. Pure operation-based CRDTs provide a unified framework for defining CRDTs based on a partially ordered log of operations. The framework eases the implementation of CRDTs and reduces the risk of introducing bugs. However, developers are still required to manually define the CRDT semantics and compaction functions, which can be complex and error-prone. This paper proposes ReDunT, a framework for the automatic synthesis of compaction functions for pure op-based CRDTs using a rewrite-based semantic approach. We evaluate ReDunT by applying it to a portfolio of pure operation-based CRDTs, including sets and flags, and comparing the obtained results with the manually optimised specifications. We also demonstrate the feasibility of the framework by implementing it as an automatic tool in K semantic framework.