Artículo

Estamos trabajando para incorporar este artículo al repositorio
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

Abstract:

Replicated data types (RDTs) concern the specification and implementation of data structures handled by replicated data stores, i.e., distributed data stores that maintain copies of the same data item on multiple devices. A distinctive feature of RDTs is that the behaviour of an operation depends on the state of the replica over which it performs, and hence, its result may differ from replica to replica. Abstractly, RDTs are specified in terms of two relations, visibility and arbitration. The former establishes whether an operation observes the effects of the execution of another operation, the latter is a total order on operations used to resolve conflicts between operations executed concurrently over different replicas. Traditionally, an operation of an RDT is specified as a function mapping a visibility and an arbitration into the expected result of the operation. This paper recasts such standard approaches into a denotational framework in which a data type is a function mapping visibility into admissible arbitrations. This characterisation provides a more abstract view of RDTs that (i) highlights some implicit assumptions shared in operational approaches to specification; (ii) accommodates underspecification and refinement; (iii) enables a direct characterisation of the correct implementations of an RDT in terms of a simulation relation between the states of a concrete implementation and of the abstract one determined by the specification. © 2018

Registro:

Documento: Artículo
Título:On the semantics and implementation of replicated data types
Autor:Gadducci, F.; Melgratti, H.; Roldán, C.
Filiación:Università di Pisa, Dipartimento di Informatica, Pisa, Italy
Universidad de Buenos Aires, Facultad de Ciencias Exactas y Naturales, Departamento de Computación, Buenos Aires, Argentina
CONICET-Universidad de Buenos Aires, Instituto de Investigación en Ciencias de la Computación (ICC), Buenos Aires, Argentina
Palabras clave:Implementation correctness; Replicated data types; Specification; Mapping; Semantics; Visibility; Distributed data stores; Function mapping; Implementation correctness; Multiple devices; Replicated data; Simulation relation; Total order; Underspecification; Specifications
Año:2018
Volumen:167
Página de inicio:91
Página de fin:113
DOI: http://dx.doi.org/10.1016/j.scico.2018.06.003
Título revista:Science of Computer Programming
Título revista abreviado:Sci Comput Program
ISSN:01676423
CODEN:SCPGD
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_01676423_v167_n_p91_Gadducci

Referencias:

  • 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
  • Shapiro, M., Preguiça, N.M., Baquero, C., Zawirski, M., Conflict-free replicated data types (2011) SSS 2011, Lect. Notes Comput. Sci., 6976, pp. 386-400. , X. Défago F. Petit V. Villain Springer
  • Burckhardt, S., Gotsman, A., Yang, H., Zawirski, M., Replicated data types: specification, verification, optimality (2014) POPL 2014, pp. 271-284. , S. Jagannathan P. Sewell ACM
  • Burckhardt, S., Principles of eventual consistency (2014) Found. Trends Program. Lang., 1 (1-2), pp. 1-150
  • Burckhardt, S., Gotsman, A., Yang, H., Understanding eventual consistency (2013), Tech. Rep. MSR-TR-2013-39 Microsoft Research; Gotsman, A., Yang, H., Composite replicated data types (2015) ESOP 2015, Lect. Notes Comput. Sci., 9032, pp. 585-609. , J. Vitek Springer
  • Cerone, A., Bernardi, G., Gotsman, A., A framework for transactional consistency models with atomic visibility (2015) CONCUR 2015, LIPIcs, 42, pp. 58-71. , L. Aceto D. de Frutos-Escrig Schloss Dagstuhl – Leibniz-Zentrum für Informatik
  • Sivaramakrishnan, K.C., Kaki, G., Jagannathan, S., Declarative programming over eventually consistent data stores (2015) PLDI 2015, pp. 413-424. , D. Grove S. Blackburn ACM
  • 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. , R. Bodík R. Majumdar ACM
  • Wirsing, M., Algebraic specification (1990) Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics (B), pp. 675-788. , Elsevier
  • Guttag, J.V., Horowitz, E., Musser, D.R., The design of data type specifications (1976) ICSE 1976, pp. 414-420. , R.T. Yeh C.V. Ramamoorthy IEEE Computer Society Press
  • Ehrich, H.-D., On the theory of specification, implementation, and parametrization of abstract data types (1982) J. ACM, 29 (1), pp. 206-227
  • Gadducci, F., Melgratti, H.C., Roldán, C., A denotational view of replicated data types (2017) COORDINATION 2017, Lect. Notes Comput. Sci., 10319, pp. 138-156. , J. Jacquet M. Massink Springer
  • Shapiro, M., Preguiça, N., Baquero, C., Zawirski, M., A comprehensive study of convergent and commutative replicated data types (2011), Tech. Rep. RR-7506 Inria-Centre Paris-Rocquencourt; Terry, D.B., Theimer, M., Petersen, K., Demers, A.J., Spreitzer, M., Hauser, C., Managing update conflicts in Bayou, a weakly connected replicated storage system (1995) SOSP 1995, pp. 172-183. , M.B. Jones ACM
  • Jagadeesan, R., Riely, J., From sequential specifications to eventual consistency (2015) ICALP 2015, Lect. Notes Comput. Sci., 9135, pp. 247-259. , M.M. Halldórsson K. Iwama N. Kobayashi B. Speckmann Springer
  • Bouajjani, A., Enea, C., Hamza, J., Verifying eventual consistency of optimistic replication systems (2014) POPL 2014, pp. 285-296. , S. Jagannathan P. Sewell ACM
  • von Gleissenthall, K., Rybalchenko, A., An epistemic perspective on consistency of concurrent computations (2013) CONCUR 2013, Lect. Notes Comput. Sci., 8052, pp. 212-226. , P.R. D'Argenio H.C. Melgratti Springer
  • Zeller, P., Bieniusa, A., Poetzsch-Heffter, A., Formal specification and verification of CRDTs (2014) FORTE 2014, Lect. Notes Comput. Sci., 8461, pp. 33-48. , E. Ábrahám C. Palamidessi Springer

Citas:

---------- APA ----------
Gadducci, F., Melgratti, H. & Roldán, C. (2018) . On the semantics and implementation of replicated data types. Science of Computer Programming, 167, 91-113.
http://dx.doi.org/10.1016/j.scico.2018.06.003
---------- CHICAGO ----------
Gadducci, F., Melgratti, H., Roldán, C. "On the semantics and implementation of replicated data types" . Science of Computer Programming 167 (2018) : 91-113.
http://dx.doi.org/10.1016/j.scico.2018.06.003
---------- MLA ----------
Gadducci, F., Melgratti, H., Roldán, C. "On the semantics and implementation of replicated data types" . Science of Computer Programming, vol. 167, 2018, pp. 91-113.
http://dx.doi.org/10.1016/j.scico.2018.06.003
---------- VANCOUVER ----------
Gadducci, F., Melgratti, H., Roldán, C. On the semantics and implementation of replicated data types. Sci Comput Program. 2018;167:91-113.
http://dx.doi.org/10.1016/j.scico.2018.06.003