Theoretical Aspects of Computing - ICTAC 2020 - 17th International Colloquium, Macau, China, November 30 - December 4, 2020, Proceedings
Theoretical Aspects of Computing - ICTAC 2020 - 17th International Colloquium, Macau, China, November 30 - December 4, 2020, Proceedings
复制标题
计算的理论方面 - ICTAC 2020 - 第十七届国际学术讨论会，中国澳门，2020 年 11 月 30 日至 12 月 4 日，会议记录
DOI：
10.1007/978-3-030-64276-1_15
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Gadducci F
中科院分区：
文献类型：
--
作者：
Gadducci F
复制数据类型（RDT）是作为处理弱一致性数据存储的抽象而引入的，弱一致性数据存储可能（临时）暴露其状态的多个不一致视图。在文献中，RDTS通常是在集合理论方面：只有最近不同的规格风味已被提出，其中一个指称的形式主义，除其他外，捕捉规范细化。然而，到目前为止，还没有抽象的模型已经提出的实现和它们的正确性方面的规范。本文填补了这一差距：我们首先给出了分类结构，用于从规范中提取操作模型，以及其实现，然后我们通过模拟定义了实现正确性的概念。
Replicated Data Types (rdts) have been introduced as an abstraction for dealing with weakly consistent data stores, which may (temporarily) expose multiple, inconsistent views of their state. In the literature,rdts are usually presented in set-theoretical terms: Only recently different specification flavours have been proposed, among them a denotational formalism that inter alia captures specification refinement. So far, however, no abstract model has been proposed for the implementations and their correctness with respect to specifications. This paper fills the gap: We first give categorical constructions for distilling an operational model from a specification, as well as its implementations, and then we define a notion of implementation correctness via simulation.