We address the fundamental issue of interfaces that arises in the context of cloud computing; namely, what does it mean for a replicated and distributed implementation of a data structure to satisfy its standard sequential specification. The main contribution of this paper is a new definition of eventual consistency that liberalizes the linear time regime of linearizability to partial orders. Any implementation that conforms to our definitions satisfies the Principle of Permutation Equivalence enunciated in the literature : “If all sequential permutations of updates lead to equivalent states, then it should also hold that concurrent executions of the updates lead to equivalent states.” Our definition also coincides with linearizability when the system is only accessed at a single replica, or when the system follows a single-master regime. More generally, we establish the following key properties: Expressiveness: We account for a wide range of extant replicated implementations of distributed data structures, including ORSET [Shapiro, Preguiça, Baquero, and Zawirski 2011] and Collaborative Text Editors [Attiya, Burckhardt, Gotsman, Morrison, Yang, and Zawirski 2016]. Composition: We show how to reason about composite data structures in terms of their components, in the style of Herlihy and Wing . This enables us to reason with a distributed implementation of a composite object (e.g., a graph) by compositionally building on assumptions about the simpler distributed objects (e.g., sets implementing vertices and sets implementing edges). Abstraction: We prove an abstraction theorem in the style of Filipovic, O’Hearn, Rinetzky, and Yang . This demonstrates how a client’s view of the distributed data structure can be simplified to reasoning with an automaton generated from the sequential specification.
Download Full PDF Version (Non-Commercial Use)