Hampa: Solver-Aided Recency-Aware Replication

Hampa: Solver-Aided Recency-Aware Replication
复制标题

DOI:
10.1007/978-3-030-53288-8_16
复制
发表时间:
2020-06-13
期刊:
Computer Aided Verification
影响因子:
--
通讯作者:
Lesani M
Lesani M
中科院分区:
其他
文献类型:
--
作者:
Li X;Houshmand F;Lesani M

文献摘要

参考文献

相似文献

复制是构建可靠和可伸缩系统的常用技术。传统的强一致性在副本之间保持相同的操作总顺序。这种整体秩序是多个理想的一致性属性的来源:完整性,收敛性和新近性。然而,维持总订单已被证明会抑制可用性和性能。较弱的概念表现出响应性和可伸缩性;然而,它们丧失了整体秩序,因此丧失了其有利的属性。该项目尽可能少地协调这些属性。它提出了一种工具,称为给定一个顺序对象的声明,其完整性和新近性的要求,自动合成一个正确的复制对象,同时保证这三个属性。它的特点是一个关系对象规范语言和语法导向的分析,推断最佳陈旧界限。此外,它定义了协调避免条件和可证明地保证这三个属性的复制系统的操作语义。它的计算能力的特点,并提出了一个协议,最近意识到的对象。 静态使用自动求解器并将其嵌入运行时中,以动态决定协调避免条件的有效性。实验表明,最近感知对象减少协调和响应时间。
Replication is a common technique to build reliable and scalable systems. Traditional strong consistency maintains the same total order of operations across replicas. This total order is the source of multiple desirable consistency properties: integrity, convergence and recency. However, maintaining the total order has proven to inhibit availability and performance. Weaker notions exhibit responsiveness and scalability; however, they forfeit the total order and hence its favorable properties. This project revives these properties with as little coordination as possible. It presents a tool called that given a sequential object with the declaration of its integrity and recency requirements, automatically synthesizes a correct-by-construction replicated object that simultaneously guarantees the three properties. It features a relational object specification language and a syntax-directed analysis that infers optimum staleness bounds. Further, it defines coordination-avoidance conditions and the operational semantics of replicated systems that provably guarantees the three properties. It characterizes the computational power and presents a protocol for recency-aware objects. uses automatic solvers statically and embeds them in the runtime to dynamically decide the validity of coordination-avoidance conditions. The experiments show that recency-aware objects reduce coordination and response time.
DOI: 10.14778/2212351.2212359
发表时间: 2012-04-01
影响因子: 2.5
作者:
Bailis, Peter;Venkataraman, Shivaram;Stoica, Ion
通讯作者: Stoica, Ion
DOI: 10.1145/2914770.2837650
发表时间: 2016-01-01
影响因子: --
作者:
Dragoi, Cezara;Henzinger, Thomas A.;Zufferey, Damien
通讯作者: Zufferey, Damien
DOI: 10.1145/2491245
发表时间: 2013-08-01
影响因子: 1.5
作者:
Corbett, James C.;Dean, Jeffrey;Woodford, Dale
通讯作者: Woodford, Dale
DOI: 10.1145/2535838.2535848
发表时间: 2014-01-01
影响因子: --
作者:
Burckhardt, Sebastian;Gotsman, Alexey;Zawirski, Marek
通讯作者: Zawirski, Marek
DOI: 10.1007/bf01784241
发表时间: 1995-08-01
影响因子: 1.3
作者:
AHAMAD, M;NEIGER, G;HUTTO, PW
通讯作者: HUTTO, PW