On the semantics and implementation of replicated data types
On the semantics and implementation of replicated data types
复制标题
关于复制数据类型的语义和实现
DOI：
10.1016/j.scico.2018.06.003
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Christian Roldán
中科院分区：
文献类型：
--
作者：
F. Gadducci;Hernán C. Melgratti;Christian Roldán
复制数据类型 (rdts) 涉及复制数据存储处理的数据结构的规范和实现，即在多个设备上维护相同数据项副本的分布式数据存储。 rdts 的一个显着特征是操作的行为取决于其执行的副本的状态，因此，其结果可能因副本而异。抽象地说，rdts是根据可见性和仲裁这两种关系来指定的。前者确定一个操作是否观察另一个操作的执行效果，后者是用于解决在不同副本上并发执行的操作之间的冲突的操作的总顺序。传统上，anrd的操作被指定为将可见性和仲裁映射到操作的预期结果的函数。本文将这些标准方法重新构建为一个指称框架，其中数据类型是将可见性映射到可接受的仲裁的函数。这种特征提供了一个更抽象的 RDTS 视图，即 (i) 强调了规范操作方法中共享的一些隐含假设； (ii) 适应规格不足和细化； (iii)能够直接表征具体实现的状态和由规范确定的抽象实现的状态之间的模拟关系的正确实现和项。
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 ofrdts 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. Abstractly,rdts are specified in terms of two relations,visibilityandarbitration. 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 anrdtis 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 ofrdts 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 anrdtin terms of a simulation relation between the states of a concrete implementation and of the abstract one determined by the specification.