A Generic Specification Framework for Weakly Consistent Replicated Data Types

Recently Burckhardt et al. proposed a formal specification framework for eventually consistent replicated data types, denoted (vis, ar), based on the notions of visibility and arbitration relations. However, being specific to eventually consistent systems, this framework has two limitations. First, it does not cover non-convergent consistency models since arbitration ar is defined to be a total order over events in a computation. Second, it does not cover the consistency models in which each event is required to be aware of the return values of some or all events that are visible to it.In this paper, we extend the (vis, ar) specification framework into a more generic one called (vis, ar, V) for weakly consistent replicated data types. To specify non-convergent consistency models as well, we simply relax the arbitration relation ar to be a partial order. To overcome the second limitation, we allow to specify for each event e, a subset V(e) of its visible set whose return values cannot be ignored when justifying the return value of e. To make it practically feasible, we provide candidates for the visibility and arbitration relations and the V function. By combining these candidates, we demonstrate how to specify various existing consistency models in the (vis, ar, V) framework. Moreover, it helps to discover new consistency models. As a case study, we prove that the causal consistency protocol of MongoDB database satisfies Causal Memory Convergence, a new causal consistency variant discovered in our framework.