On the semantics and implementation of replicated data types

Replicated data types (rdts) concern the specification and implementation of data structures handled by replicated data stores, i.e., distributed data stores that maintain copies of the same data item on multiple devices. A distinctive feature of rdts is that the behaviour of an operation depends on the state of the replica over which it performs, and hence, its result may differ from replica to replica. ly, rdts are specified in terms of two relations, visibility and arbitration. The former establishes whether an operation observes the effects of the execution of another operation, the latter is a total order on operations used to resolve conflicts between operations executed concurrently over different replicas. Traditionally, an operation of an rdt is specified as a function mapping a visibility and an arbitration into the expected result of the operation. This paper recasts such standard approaches into a denotational framework in which a data type is a function mapping visibility into admissible arbitrations. This characterisation provides a more abstract view of rdts that (i) highlights some implicit assumptions shared in operational approaches to specification; (ii) accommodates underspecification and refinement; (iii) enables a direct characterisation of the correct implementations of an rdt in terms of a simulation relation between the states of a concrete implementation and of the abstract one determined by the specification.