Navegar

Colección

Datos Estadísticas

Artículo

Melgratti, H.; Roldán, C.; Lafuente A.L.; Proenca J. "A formal analysis of the global sequence protocol" (2016) 18th IFIP WG 6.1 International Conference on Coordination Models and Languages, COORDINATION 2016 and Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016. 9686:175-191
El editor solo permite decargar el artículo en su versión post-print desde el repositorio. Por favor, si usted posee dicha versión, enviela a
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

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. © IFIP International Federation for Information Processing 2016.

Registro:

Documento: Artículo
Título:A formal analysis of the global sequence protocol
Autor:Melgratti, H.; Roldán, C.; Lafuente A.L.; Proenca J.
Filiación:Departamento de Computación, FCEyN, Universidad de Buenos Aires, Buenos Aires, Argentina
CONICET, Buenos Aires, Argentina
Palabras clave:Computational linguistics; Distributed computer systems; Formal methods; Communication failure; Compact representation; Execution history; Formal analysis; Operational model; Replicated data; Sequence protocols; Strong consistency; Calculations
Año:2016
Volumen:9686
Página de inicio:175
Página de fin:191
DOI: http://dx.doi.org/10.1007/978-3-319-39519-7_11
Título revista:18th IFIP WG 6.1 International Conference on Coordination Models and Languages, COORDINATION 2016 and Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016
Título revista abreviado:Lect. Notes Comput. Sci.
ISSN:03029743
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v9686_n_p175_Melgratti

Referencias:

  • Bailis, P., Ghodsi, A., Eventual consistency today: Limitations, extensions, and beyond (2013) Commun. ACM, 56 (5), pp. 55-63
  • Burckhardt, S., Principles of eventual consistency (2014) Found. Trends Program. Lang, 1 (1-2), pp. 1-150
  • Burckhardt, S., Fähndrich, M., Leijen, D., Wood, B.P., Cloud types for eventual consistency (2012) ECOOP 2012. LNCS, 7313, pp. 283-307. , Noble, J. (ed.), Springer, Heidelberg
  • Burckhardt, S., Leijen, D., Fähndrich, M., Sagiv, M., Eventually consistent transactions (2012) Programming Languages and Systems. LNCS, 7211, pp. 67-86. , Seidl, H. (ed.), Springer, Heidelberg
  • Burckhardt, S., Leijen, D., Protzenko, J., Fähndrich, M., Global sequence protocol: A robust abstraction for replicated shared state (2015) ECOOP 2015, pp. 568-590
  • Decandia, G., Hastorun, D., Jampani, M., Kakulapati, G., Lakshman, A., Pilchin, A., Sivasubramanian, S., Vogels, W., Dynamo: Amazon’s highly available key-value store (2007) SOSP 2007, pp. 205-220. , ACM
  • Gilbert, S., Lynch, N., Brewer’s conjecture and the feasibility of consistent, available, partition-tolerant web services (2002) SIGACT News, 33 (2), pp. 51-59
  • Gotsman, A., Yang, H., Ferreira, C., Najafzadeh, M., Shapiro, M., ‘Cause i’m strong enough: Reasoning about consistency choices in distributed systems (2016) POPL 2016, pp. 371-384
  • Lakshman, A., Malik, P., Cassandra: A decentralized structured storage system (2010) ACM SIGOPS Operating Syst. Rev, 44 (2), pp. 35-40
  • Shapiro, M., Preguiça, N., Baquero, C., Zawirski, M., Conflict-free replicated data types (2011) SSS 2011. LNCS, 6976, pp. 386-400. , Défago, X., Petit, F., Villain, V. (eds.), Springer, Heidelberg
  • Sivaramakrishnan, K., Kaki, G., Jagannathan, S., Declarative programming over eventually consistent data stores (2015) PLDI 2015, pp. 413-424. , ACMA4 -

Citas:

---------- APA ----------
Melgratti, H., Roldán, C., Lafuente A.L. & Proenca J. (2016) . A formal analysis of the global sequence protocol. 18th IFIP WG 6.1 International Conference on Coordination Models and Languages, COORDINATION 2016 and Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016, 9686, 175-191.
http://dx.doi.org/10.1007/978-3-319-39519-7_11
---------- CHICAGO ----------
Melgratti, H., Roldán, C., Lafuente A.L., Proenca J. "A formal analysis of the global sequence protocol" . 18th IFIP WG 6.1 International Conference on Coordination Models and Languages, COORDINATION 2016 and Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016 9686 (2016) : 175-191.
http://dx.doi.org/10.1007/978-3-319-39519-7_11
---------- MLA ----------
Melgratti, H., Roldán, C., Lafuente A.L., Proenca J. "A formal analysis of the global sequence protocol" . 18th IFIP WG 6.1 International Conference on Coordination Models and Languages, COORDINATION 2016 and Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016, vol. 9686, 2016, pp. 175-191.
http://dx.doi.org/10.1007/978-3-319-39519-7_11
---------- VANCOUVER ----------
Melgratti, H., Roldán, C., Lafuente A.L., Proenca J. A formal analysis of the global sequence protocol. Lect. Notes Comput. Sci. 2016;9686:175-191.
http://dx.doi.org/10.1007/978-3-319-39519-7_11