Safe Replication through Bounded Concurrency Verification
Safe Replication through Bounded Concurrency Verification
复制标题
DOI：
10.1145/3276534
复制
发表时间：
2018-11-01
影响因子：
1.8
通讯作者：
Jagannathan, Suresh
中科院分区：
文献类型：
--
作者：
Kaki, Gowtham;Earanky, Kapil;Jagannathan, Suresh
高级数据类型通常与语义不变量相关联，任何正确的实现都必须保留这些语义不变量。虽然实现强制执行强有力的保证（例如线性化或串行化）通常可用于防止并发设置中的不变性违规，但这种机制在地理分布式复制环境（许多可扩展 Web 服务的首选平台）中是不切实际的。为了实现该领域所必需的高可用性，这些环境允许各种形式的弱一致性，但不能保证所有副本都具有应用程序状态的一致视图。因此，他们经常承认难以理解的异常行为，这些行为违反了数据类型的不变量，但即使对于专家来说，理解和调试这些行为也极具挑战性。在本文中，我们提出了一种用于复制数据类型（RDT）的新型编程框架，配备了自动（有界）验证技术，可以发现并修复弱一致性异常。我们的方法在名为 Q9 的工具中实现，涉及系统地探索在最终一致的数据存储之上执行的应用程序的状态空间，在不受限制的一致性模型下但具有有限的并发限制。 Q9 发现表现为有限反例的异常（即不变违规），并通过有选择地加强特定操作的一致性保证来自动生成此类异常的修复。使用 Q9，我们发现了著名基准测试实施中的一系列细微异常，并能够应用它要求的修复来有效消除这些异常。值得注意的是，这些基准测试是采用建议管理分布式复制状态的最佳实践编写的（例如，它们由可证明收敛的 RDT（CRDT）组成，避免可变状态等）。虽然我们的技术提供的安全保证受到并发界限的限制，但我们表明，在实践中，证明有界安全保证通常可以推广到无界情况。
High-level data types are often associated with semantic invariants that must be preserved by any correct implementation. While having implementations enforce strong guarantees such as linearizability or serializability can often be used to prevent invariant violations in concurrent settings, such mechanisms are impractical in geo-distributed replicated environments, the platform of choice for many scalable Web services. To achieve high-availability essential to this domain, these environments admit various forms of weak consistency that do not guarantee all replicas have a consistent view of an application's state. Consequently, they often admit difficult-to-understand anomalous behaviors that violate a data type's invariants, but which are extremely challenging, even for experts, to understand and debug.In this paper, we propose a novel programming framework for replicated data types (RDTs) equipped with an automatic (bounded) verification technique that discovers and fixes weak consistency anomalies. Our approach, implemented in a tool called Q9, involves systematically exploring the state space of an application executing on top of an eventually consistent data store, under an unrestricted consistency model but with a finite concurrency bound. Q9 uncovers anomalies (i.e., invariant violations) that manifest as finite counterexamples, and automatically generates repairs for such anomalies by selectively strengthening consistency guarantees for specific operations. Using Q9, we have uncovered a range of subtle anomalies in implementations of well-known benchmarks, and have been able to apply the repairs it mandates to effectively eliminate them. Notably, these benchmarks were written adopting best practices suggested to manage distributed replicated state (e.g., they are composed of provably convergent RDTs (CRDTs), avoid mutable state, etc.). While the safety guarantees offered by our technique are constrained by the concurrency bound, we show that in practice, proving bounded safety guarantees typically generalizes to the unbounded case.