一句话：自动分析顺序对象的冲突与依赖关系，并为分布式复制合成避免不必要协调且满足完整性与收敛的对象。
分布式复制广泛用于容错与扩展，但多种一致性选择使客户端在正确性、响应性和可用性之间面临两难。本文给定顺序对象及其完整性属性，自动合成一个保证状态完整性与收敛并避免不必要协调的复制对象。方法的核心是名为 well-coordination 的充分条件，它要求冲突与依赖操作之间满足特定顺序；系统静态分析顺序对象以判定冲突和依赖方法，并实例化参数化的新协调协议来满足该条件。作者实现工具 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.
@article{paperbot683,
title = {Hamsaz: replication coordination analysis and synthesis},
author = {Farzin Houshmand and Mohsen Lesani},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290387}
}