1: \begin{abstract}

2:   

3: Maintaining multiple replicas of data is crucial to achieving

4: scalability, availability and low latency in distributed

5: applications. \emph{Conflict-free Replicated Data Types} (CRDTs) are

6: important building blocks in this domain because they are designed to

7: operate correctly under the myriad behaviors possible in a

8: weakly-consistent distributed setting.  Because of the possibility of

9: concurrent updates to the same object at different replicas, and the

10: absence of any ordering guarantees on these updates,

11: \emph{convergence} is an important correctness criterion for CRDTs.

12: This property asserts that two replicas which receive the same set of

13: updates (in any order) must nonetheless converge to the same state.

14: One way to prove that operations on a CRDT converge is to show that

15: they commute since commutative actions by definition behave the same

16: regardless of the order in which they execute.  In this paper, we

17: present a framework for automatically verifying convergence of CRDTs under different

18: weak-consistency policies.  Surprisingly, depending upon the

19: consistency policy supported by the underlying system, we show that

20: not all operations of a CRDT need to commute to achieve convergence.

21: We develop a proof rule parameterized by a consistency specification

22: based on the concepts of \emph{commutativity modulo consistency

23:   policy} and \emph{non-interference to commutativity}.  We describe

24: the design and implementation of a verification engine equipped with

25: this rule and show how it can be used to provide the first automated

26: convergence proofs for a number of challenging CRDTs, including sets,

27: lists, and graphs.

28: 

29: %\keywords{First keyword  \and Second keyword \and Another keyword.}

30: \end{abstract}

31: