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...

Descripción completa

Detalles Bibliográficos
Autores principales: Li, Xiao, Houshmand, Farzin, Lesani, Mohsen
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