论文标题
Visearch:复制数据类型的弱一致性测量
ViSearch: Weak Consistency Measurement for Replicated Data Types
论文作者
论文摘要
大规模复制的数据类型商店通常会诉诸最终的一致性,以确保低潜伏期和高可用性。人们普遍认为,由于允许复制品之间的任意分歧,因此最终对一致的数据存储进行编程是具有挑战性的。此外,务实协议实际上达到的一致性比最终的一致性更强,这可以并且需要使用,以促进对复制数据类型的推理和编程。面对上面的挑战,我们提出了Visearch框架,以精确测量最终的一致性语义。 Visearch在并发编程中采用可见性 - 弧度规范方法,该方法扩展了基于线性的规范方法,以及操作之间的动态可见性关系,除了标准的动态事件和线性化关系。使用Visearch的一致性测量通常是NP-HARD。为了在复制的数据类型存储中实现实用,有效的一致性测量,Visearch框架对现有的蛮力检查算法进行了重构为通用算法骨架,从而进一步有效地修剪了搜索空间和有效的并行化。我们采用Visearch框架在两个复制的数据类型存储Riak和Crdt-Redis中进行一致性测量。实验评估显示了基于现实情况下的Visearch框架一致性测量的有用性和成本效益。
Large-scale replicated data type stores often resort to eventual consistency to guarantee low latency and high availability. It is widely accepted that programming over eventually consistent data stores is challenging, since arbitrary divergence among replicas is allowed. Moreover, pragmatic protocols actually achieve consistency guarantees stronger than eventual consistency, which can be and need to be utilized to facilitate the reasoning of and programming over replicated data types. Toward the challenges above, we propose the ViSearch framework for precise measurement of eventual consistency semantics. ViSearch employs the visibility-arbitration specification methodology in concurrent programming, which extends the linearizability-based specification methodology with a dynamic visibility relation among operations, in addition to the standard dynamic happen-before and linearization relations. The consistency measurement using ViSearch is NP-hard in general. To enable practical and efficient consistency measurement in replicated data type stores, the ViSearch framework refactors the existing brute-force checking algorithm to a generic algorithm skeleton, which further enables efficient pruning of the search space and effective parallelization. We employ the ViSearch framework for consistency measurement in two replicated data type stores Riak and CRDT-Redis. The experimental evaluation shows the usefulness and cost-effectiveness of consistency measurement based on the ViSearch framework in realistic scenarios.