A Formal Analysis of the Global Sequence Protocol

Abstract : 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.
Complete list of metadatas

Cited literature [11 references]  Display  Hide  Download

https://hal.inria.fr/hal-01631716
Contributor : Hal Ifip <>
Submitted on : Thursday, November 9, 2017 - 4:13:48 PM
Last modification on : Wednesday, April 17, 2019 - 4:06:02 PM
Long-term archiving on : Saturday, February 10, 2018 - 2:28:00 PM

File

416253_1_En_11_Chapter.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Hernán Melgratti, Christian Roldán. A Formal Analysis of the Global Sequence Protocol. 18th International Conference on Coordination Languages and Models (COORDINATION), Jun 2016, Heraklion, Greece. pp.175-191, ⟨10.1007/978-3-319-39519-7_11⟩. ⟨hal-01631716⟩

Share

Metrics

Record views

47

Files downloads

210