Hamsaz: Replication Coordination Analysis and Synthesis
Hamsaz: Replication Coordination Analysis and Synthesis
复制标题
DOI：
10.1145/3290387
复制
发表时间：
2019-01-01
影响因子：
1.8
通讯作者：
Lesani, Mohsen
中科院分区：
文献类型：
--
作者：
Houshmand, Farzin;Lesani, Mohsen
分布式系统复制作为一种容错和可伸缩的手段被广泛使用。然而，它提供了一系列的一致性选择，使客户端在正确性、响应性和可用性之间陷入困境。给定一个顺序对象及其完整性属性，我们自动合成一个复制对象，保证状态的完整性和收敛性，并避免不必要的协调。我们的方法是基于一个新的完整性和收敛的充分条件称为良好的协调，需要一定的顺序之间的冲突和依赖的操作。我们静态分析给定的顺序对象，以确定其冲突和依赖的方法，并使用这些信息，以避免协调。我们提出了新的协调协议，参数的分析结果，并提供良好的协调要求。我们实现了一个名为Hamsaz的工具，可以自动分析给定的对象，实例化的协议和合成复制的对象。我们已经将Hamsaz应用于一组用例，并合成了比强一致基线响应更快的复制对象。
Distributed system replication is widely used as a means of fault-tolerance and scalability. However, it provides a spectrum of consistency choices that impose a dilemma for clients between correctness, responsiveness and availability. Given a sequential object and its integrity properties, we automatically synthesize a replicated object that guarantees state integrity and convergence and avoids unnecessary coordination. Our approach is based on a novel sufficient condition for integrity and convergence called well-coordination that requires certain orders between conflicting and dependent operations. We statically analyze the given sequential object to decide its conflicting and dependent methods and use this information to avoid coordination. We present novel coordination protocols that are parametric in terms of the analysis results and provide the well-coordination requirements. We implemented a tool called Hamsaz that can automatically analyze the given object, instantiate the protocols and synthesize replicated objects. We have applied Hamsaz to a suite of use-cases and synthesized replicated objects that are significantly more responsive than the strongly consistent baseline.