复制系统中并发库的语义、规范和有界验证
Semantics, Specification, and Bounded Verification of Concurrent Libraries in Replicated Systems
AI总结：
本文针对地理复制系统中的弱一致性并发库，提出语义与规范，并开发静态分析框架以自动检测正确性违规，首次证明此类自动检查可行且实用。
摘要：
地理复制系统提供了许多理想的特性，例如全局低延迟、高可用性、可扩展性和内置的容错能力。不幸的是，在此类系统之上编写正确的应用程序已被证明极具挑战性，这在很大程度上是因为它们提供的弱一致性保证。当我们尝试将专为共享内存环境开发的高性能并发库适应到这种设置时，这些复杂性会进一步加剧。使用这些以性能和可扩展性为设计目标的库是非常可取的。但是，在弱一致性执行模型下，确定一个合适的正确性概念来检验其有效性尚未得到充分研究，这在很大程度上是因为天真地移植诸如线性化之类的标准（该标准在共享内存上下文中有有用的解释）到分布式环境（其中对所有操作施加（逻辑上的）全局排序的成本过高）是有问题的。在本文中，我们通过为弱一致性、复制设置中的高并发库提出适当的语义和规范来解决这些问题。我们使用这些规范开发了一个静态分析框架，该框架可以自动检测库实现的正确性违规，这些实现以底层系统提供的不同一致性策略为参数。我们使用我们的框架来分析栈、队列和交换器的多个高度非平凡的库实现的行为。我们的结果首次证明，在弱地理复制设置中，并发库的自动正确性检查既可行又实用。
英文摘要：
Geo-replicated systems provide a number of desirable properties such as globally low latency, high availability, scalability, and built-in fault tolerance. Unfortunately, programming correct applications on top of such systems has proven to be very challenging, in large part because of the weak consistency guarantees they offer. These complexities are exacerbated when we try to adapt existing highly-performant concurrent libraries developed for shared-memory environments to this setting. The use of these libraries, developed with performance and scalability in mind, is highly desirable. But, identifying a suitable notion of correctness to check their validity under a weakly consistent execution model has not been well-studied, in large part because it is problematic to naively transplant criteria such as linearizability that has a useful interpretation in a shared-memory context to a distributed one where the cost of imposing a (logical) global ordering on all actions is prohibitive. In this paper, we tackle these issues by proposing appropriate semantics and specifications for highly-concurrent libraries in a weakly-consistent, replicated setting. We use these specifications to develop a static analysis framework that can automatically detect correctness violations of library implementations parameterized with respect to the different consistency policies provided by the underlying system. We use our framework to analyze the behavior of a number of highly non-trivial library implementations of stacks, queues, and exchangers. Our results provide the first demonstration that automated correctness checking of concurrent libraries in a weakly geo-replicated setting is both feasible and practical.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
