A formal analysis of the global sequence protocol

The Global Sequence Protocol (GSP) is an operational model for replicated data stores, in which updates propagate asynchronously. We introduce the GSP-calculus as a formal model for GSP. We give a formal account for its proposed implementation, which addresses communication failures and compact repr...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Melgratti, H., Roldán, C., Lafuente A.L., Proenca J.
Formato: SER
Materias:
Computational linguistics
Distributed computer systems
Formal methods
Communication failure
Compact representation
Execution history
Formal analysis
Operational model
Replicated data
Sequence protocols
Strong consistency
Calculations
Acceso en línea:http://hdl.handle.net/20.500.12110/paper_03029743_v9686_n_p175_Melgratti
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id todo:paper_03029743_v9686_n_p175_Melgratti
record_format dspace
spelling todo:paper_03029743_v9686_n_p175_Melgratti2023-10-03T15:19:42Z A formal analysis of the global sequence protocol Melgratti, H. Roldán, C. Lafuente A.L. Proenca J. Computational linguistics Distributed computer systems Formal methods Communication failure Compact representation Execution history Formal analysis Operational model Replicated data Sequence protocols Strong consistency Calculations The Global Sequence Protocol (GSP) is an operational model for replicated data stores, in which updates propagate asynchronously. We introduce the GSP-calculus as a formal model for GSP. We give a formal account for its proposed implementation, which addresses communication failures and compact representation of data, and use simulation to prove that the implementation is correct. Then, we use the GSP-calculus to reason about execution histories and prove ordering guarantees, such as read my writes, monotonic reads, causality and consistent prefix. We also prove that GSP extended with synchronous updates provides strong consistency guarantees. © IFIP International Federation for Information Processing 2016. SER info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_03029743_v9686_n_p175_Melgratti
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic Computational linguistics
Distributed computer systems
Formal methods
Communication failure
Compact representation
Execution history
Formal analysis
Operational model
Replicated data
Sequence protocols
Strong consistency
Calculations
spellingShingle Computational linguistics
Distributed computer systems
Formal methods
Communication failure
Compact representation
Execution history
Formal analysis
Operational model
Replicated data
Sequence protocols
Strong consistency
Calculations
Melgratti, H.
Roldán, C.
Lafuente A.L.
Proenca J.
A formal analysis of the global sequence protocol
topic_facet Computational linguistics
Distributed computer systems
Formal methods
Communication failure
Compact representation
Execution history
Formal analysis
Operational model
Replicated data
Sequence protocols
Strong consistency
Calculations
description The Global Sequence Protocol (GSP) is an operational model for replicated data stores, in which updates propagate asynchronously. We introduce the GSP-calculus as a formal model for GSP. We give a formal account for its proposed implementation, which addresses communication failures and compact representation of data, and use simulation to prove that the implementation is correct. Then, we use the GSP-calculus to reason about execution histories and prove ordering guarantees, such as read my writes, monotonic reads, causality and consistent prefix. We also prove that GSP extended with synchronous updates provides strong consistency guarantees. © IFIP International Federation for Information Processing 2016.
format SER
author Melgratti, H.
Roldán, C.
Lafuente A.L.
Proenca J.
author_facet Melgratti, H.
Roldán, C.
Lafuente A.L.
Proenca J.
author_sort Melgratti, H.
title A formal analysis of the global sequence protocol
title_short A formal analysis of the global sequence protocol
title_full A formal analysis of the global sequence protocol
title_fullStr A formal analysis of the global sequence protocol
title_full_unstemmed A formal analysis of the global sequence protocol
title_sort formal analysis of the global sequence protocol
url http://hdl.handle.net/20.500.12110/paper_03029743_v9686_n_p175_Melgratti
work_keys_str_mv AT melgrattih aformalanalysisoftheglobalsequenceprotocol
AT roldanc aformalanalysisoftheglobalsequenceprotocol
AT lafuenteal aformalanalysisoftheglobalsequenceprotocol
AT proencaj aformalanalysisoftheglobalsequenceprotocol
AT melgrattih formalanalysisoftheglobalsequenceprotocol
AT roldanc formalanalysisoftheglobalsequenceprotocol
AT lafuenteal formalanalysisoftheglobalsequenceprotocol
AT proencaj formalanalysisoftheglobalsequenceprotocol
_version_ 1807321038866874368

Ejemplares similares