Cargando…
Hampa: Solver-Aided Recency-Aware Replication
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...
Autores principales: | , , |
---|---|
Formato: | Online Artículo Texto |
Lenguaje: | English |
Publicado: |
2020
|
Materias: | |
Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7363281/ http://dx.doi.org/10.1007/978-3-030-53288-8_16 |
_version_ | 1783559639494819840 |
---|---|
author | Li, Xiao Houshmand, Farzin Lesani, Mohsen |
author_facet | Li, Xiao Houshmand, Farzin Lesani, Mohsen |
author_sort | Li, Xiao |
collection | PubMed |
description | 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 [Formula: see text] 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. [Formula: see text] 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. |
format | Online Article Text |
id | pubmed-7363281 |
institution | National Center for Biotechnology Information |
language | English |
publishDate | 2020 |
record_format | MEDLINE/PubMed |
spelling | pubmed-73632812020-07-16 Hampa: Solver-Aided Recency-Aware Replication Li, Xiao Houshmand, Farzin Lesani, Mohsen Computer Aided Verification Article 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 [Formula: see text] 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. [Formula: see text] 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. 2020-06-13 /pmc/articles/PMC7363281/ http://dx.doi.org/10.1007/978-3-030-53288-8_16 Text en © The Author(s) 2020 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. |
spellingShingle | Article Li, Xiao Houshmand, Farzin Lesani, Mohsen Hampa: Solver-Aided Recency-Aware Replication |
title | Hampa: Solver-Aided Recency-Aware Replication |
title_full | Hampa: Solver-Aided Recency-Aware Replication |
title_fullStr | Hampa: Solver-Aided Recency-Aware Replication |
title_full_unstemmed | Hampa: Solver-Aided Recency-Aware Replication |
title_short | Hampa: Solver-Aided Recency-Aware Replication |
title_sort | hampa: solver-aided recency-aware replication |
topic | Article |
url | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7363281/ http://dx.doi.org/10.1007/978-3-030-53288-8_16 |
work_keys_str_mv | AT lixiao hampasolveraidedrecencyawarereplication AT houshmandfarzin hampasolveraidedrecencyawarereplication AT lesanimohsen hampasolveraidedrecencyawarereplication |