Semantics, Specification, and Bounded Verification of Concurrent Libraries in Replicated Systems
Semantics, Specification, and Bounded Verification of Concurrent Libraries in Replicated Systems
复制标题
DOI：
10.1007/978-3-030-53288-8_13
复制
发表时间：
2020-06-13
期刊：
影响因子：
--
通讯作者：
Jagannathan S
中科院分区：
文献类型：
--
作者：
Nagar K;Mukherjee P;Jagannathan S
地理复制系统提供了许多理想的特性，例如全局低延迟、高可用性、可扩展性和内置容错能力。不幸的是，事实证明，在此类系统之上编写正确的应用程序非常具有挑战性，很大程度上是因为它们提供的一致性保证很弱。当我们尝试使为共享内存环境开发的现有高性能并发库适应此设置时，这些复杂性会加剧。使用这些在开发时考虑到性能和可扩展性的库是非常可取的。但是，确定一种合适的正确性概念来检查其在弱一致性执行模型下的有效性尚未得到充分研究，这在很大程度上是因为将共享内存上下文中具有有用解释的线性化等标准移植到分布式环境中是有问题的，在分布式环境中，对所有操作强加（逻辑）全局排序的成本是令人望而却步的。在本文中，我们通过为弱一致性、复制环境中的高并发库提出适当的语义和规范来解决这些问题。我们使用这些规范来开发一个静态分析框架，该框架可以自动检测相对于底层系统提供的不同一致性策略参数化的库实现的正确性违规。我们使用我们的框架来分析许多非常重要的堆栈、队列和交换器库实现的行为。我们的结果首次证明，在弱地理复制环境中对并发库进行自动正确性检查既可行又实用。
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 naïvely 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.
登录
查看更多内容
影响因子：
1.3
作者：
HERLIHY, MP;WING, JM
通讯作者：
WING, JM
影响因子：
1.8
作者：
Kaki, Gowtham;Earanky, Kapil;Jagannathan, Suresh
通讯作者：
Jagannathan, Suresh
影响因子：
--
作者：
Emmi, Michael;Enea, Constantin;Hamza, Jad
通讯作者：
Hamza, Jad
影响因子：
--
作者：
Burckhardt, Sebastian;Gotsman, Alexey;Zawirski, Marek
通讯作者：
Zawirski, Marek
影响因子：
2.5
作者：
Bailis, Peter;Davidson, Aaron;Stoica, Ion
通讯作者：
Stoica, Ion