%0 Conference Proceedings
%T A Formal Analysis of the Global Sequence Protocol
%+ Universidad de Buenos Aires [Buenos Aires] (UBA)
%+ Consejo Nacional de Investigaciones Científicas y Técnicas [Buenos Aires] (CONICET)
%A Melgratti, Hernán
%A Roldán, Christian
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 18th International Conference on Coordination Languages and Models (COORDINATION)
%C Heraklion, Greece
%Y Alberto Lluch Lafuente
%Y José Proença
%I Springer International Publishing
%3 Coordination Models and Languages
%V LNCS-9686
%P 175-191
%8 2016-06-06
%D 2016
%R 10.1007/978-3-319-39519-7_11
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X 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.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-01631716/document
%2 https://inria.hal.science/hal-01631716/file/416253_1_En_11_Chapter.pdf
%L hal-01631716
%U https://inria.hal.science/hal-01631716
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-COORDINATION
%~ IFIP-LNCS-9686