Mergeable replicated data types
Mergeable replicated data types
复制标题
可合并的复制数据类型
DOI：
10.1145/3360580
复制
发表时间：
2019
影响因子：
--
通讯作者：
Jagannathan, Suresh
中科院分区：
文献类型：
--
作者：
Kaki, Gowtham;Priya, Swarn;Sivaramakrishnan, KC;Jagannathan, Suresh
考虑到对不同副本上的不同演化状态进行推理的复杂性，地理复制分布式系统的编程是具有挑战性的。现有的解决这个问题的方法给应用程序开发人员带来了很大的负担，他们需要考虑在一个副本上执行的操作如何被证明并应用于其他副本。为了减轻这些挑战，我们提出了一个根本不同的方法来编程中存在的复制状态。我们的洞察力是基于使用可逆的关系规范的归纳定义的数据类型作为一种机制，以捕获相关的数据类型的显着方面，其不同的实例可以安全地合并在一个复制的环境。重要的是，由于这些规范仅解决数据类型的（静态）结构属性，因此它们的制定不需要暴露关于可扩展性，复制，可见性等的低级系统级细节。因此，我们的框架能够在任意复杂的（即，可组合的）数据类型。我们表明，使用一个丰富的关系规范语言，使我们能够提取足够的条件，自动导出合并功能，有意义的非平凡的收敛特性。我们将这些想法在一个工具，称为夸克，并通过对现实世界的基准详细的评估研究，证明其实用性。
Programming geo-replicated distributed systems is challenging given the complexity of reasoning about different evolving states on different replicas. Existing approaches to this problem impose significant burden on application developers to consider the effect of how operations performed on one replica are witnessed and applied on others. To alleviate these challenges, we present a fundamentally different approach to programming in the presence of replicated state. Our insight is based on the use of invertible relational specifications of an inductively-defined data type as a mechanism to capture salient aspects of the data type relevant to how its different instances can be safely merged in a replicated environment. Importantly, because these specifications only address a data type's (static) structural properties, their formulation does not require exposing low-level system-level details concerning asynchrony, replication, visibility, etc. As a consequence, our framework enables the correct-by-construction synthesis of rich merge functions over arbitrarily complex (i.e., composable) data types. We show that the use of a rich relational specification language allows us to extract sufficient conditions to automatically derive merge functions that have meaningful non-trivial convergence properties. We incorporate these ideas in a tool called Quark, and demonstrate its utility via a detailed evaluation study on real-world benchmarks.
登录
查看更多内容
DOI：
--
发表时间：
2014
期刊：
ACM SIGPLAN International Conference on Functional Programming
影响因子：
--
作者：
Gowtham Kaki;S. Jagannathan
通讯作者：
S. Jagannathan
具有类型的红黑树
影响因子：
1.1
作者：
Stefan Kahrs
通讯作者：
Stefan Kahrs
DOI：
10.1145/343477.343502
发表时间：
2000-07
期刊：
--
影响因子：
--
作者：
E. Brewer
通讯作者：
E. Brewer
影响因子：
1.8
作者：
Kaki, Gowtham;Nagar, Kartik;Jagannathan, Suresh
通讯作者：
Jagannathan, Suresh
DOI：
--
发表时间：
2006
期刊：
影响因子：
--
作者：
C. Doczkal;Martin Erwig
通讯作者：
Martin Erwig