Especificación y semántica de tipos de datos replicados

Mostrar todas las versiones(3)

La infraestructura para almacenes de datos replicados ofrece un throughput (o latencia) bajo y la capacidad de seguir respondiendo ante la presencia de fallas. Sin embargo, un resultado conocido por la sigla CAP [1] (Consistency, Availability y Partition Tolerance) establece que no e...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Roldán, Christian Hugo
Otros Autores: Melgratti, Hernán Claudio
Formato: Tesis doctoral publishedVersion
Lenguaje:Español
Publicado: Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2020
Acceso en línea:https://hdl.handle.net/20.500.12110/tesis_n6778_Roldan
http://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesis&d=tesis_n6778_Roldan_oai
Aporte de:
Repositorio Digital de la Universidad de Buenos Aires (UBA) de Universidad de Buenos Aires
id I28-R145-tesis_n6778_Roldan_oai
record_format dspace
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-145
collection Repositorio Digital de la Universidad de Buenos Aires (UBA)
language Español
orig_language_str_mv spa
description La infraestructura para almacenes de datos replicados ofrece un throughput (o latencia) bajo y la capacidad de seguir respondiendo ante la presencia de fallas. Sin embargo, un resultado conocido por la sigla CAP [1] (Consistency, Availability y Partition Tolerance) establece que no es posible garantizar alta disponibilidad, tolerancia a fallas y consistencia (fuerte) simultáneamente. Como consecuencia, una de estas tres propiedades debe ser descartada. En la actualidad, muchas bases de datos replicadas, como Dynamo [2] o Cassandra [3] se construyen relajando la noción de consistencia y ofreciendo versiones más débiles de consistencia, conocidas generalmente como Consistencia Eventual [4]. La consistencia eventual garantiza que cualquier escritura será entregada a cada réplica del sistema y que tarde o temprano todas las réplicas convergerán a un mismo estado. Sin embargo, esto significa también, que (i) las réplicas mostrarán inconsistencia de datos (o anomalías) hasta que todas las réplicas lleguen al mismo estado y que (ii) todas las réplicas deben utilizar la misma política de resolución de conflictos ante la presencia de escrituras concurrentes con el fin de garantizar la convergencia. Las sistemas replicados adoptan diferentes estrategias para lidiar con inconsistencias temporales y resolver conflictos entre escrituras concurrentes, por ejemplo el uso de tipos de datos replicados (RDTs) [5, 6]. Por lo tanto, la solución seleccionada impacta en las propiedades aseguradas por el sistema, es decir, en el tipo de inconsistencias o anomalías que las aplicaciones permiten y observan. Dichas anomalías se caracterizan generalmente en términos de modelos de consistencia (como monotonic-read y consistencia causal) definidas axiomáticamente restringiendo las computaciones que pueden ocurrir en un sistema replicado [7, 8, 9]. Esta tesis contribuye al desarrollo de modelos de programación y técnicas de análisis para construir aplicaciones que lidien con nociones de consistencia débil. Presentamos una técnica de especificación para datos replicados cuya presentación será denotacional, para luego, movernos a una descripción categorial. Esta caracterización funcional es una propuesta alternativa a los enfoques operacionales actuales que se basan en historias abstractas [10, 11, 12, 13]. Brindamos, por lo tanto, una caracterización directa sobre la correctitud de las implementaciones de los RDTs basándonos en una relación de simulación entre los estados de una implementación concreta y los estados abstractos determinados por nuestra especificación [14]. Siguiendo el enfoque denotacional, asociamos a los tipos de datos replicados objetos matemáticos que representan su significado (es decir, definen dominios). En nuestra visión, estos objetos son funtores de PIDag(L) en SPath(L), donde PIDag(L) es la categoría de los Labelled Directed Acyclic Graphs (LDAGs) y morfismos que reflejan el pasado y SPath(L) es la categoría de conjuntos de caminos (u ordenes posibles sobre las operaciones) y morfismos entre conjuntos de caminos (que denota los ordenes admisibles). Damos una caracterización de tipos de datos replicados en término de las propiedades que los funtores gozan respecto de la flechas de PIDag(L) (por ejemplo, en término de la preservación de pullback/pushout). Como es usual con las semánticas funtoriales, la presentación categorial resultante de la actividad precedente posibilita el desarrollo de operadores adecuados para composición de especificaciones. Por último, estudiamos la semántica de programas corriendo sobre sistemas replicados, es decir, desarrollamos una caracterización alternativa para modelos de consistencia débil que son lo suficientemente general como para capturar algunos de los modelos de consistencia conocidos [15]. Mostramos algunas instanciaciones en nuestro framework y probaremos que las caracterizaciones obtenidas son sound y complete. Más aún, mostramos que a partir de este modelo se desprende una semántica denotacional de programas.
author2 Melgratti, Hernán Claudio
author_facet Melgratti, Hernán Claudio
Roldán, Christian Hugo
format Tesis doctoral
Tesis doctoral
publishedVersion
author Roldán, Christian Hugo
spellingShingle Roldán, Christian Hugo
Especificación y semántica de tipos de datos replicados
author_sort Roldán, Christian Hugo
title Especificación y semántica de tipos de datos replicados
title_short Especificación y semántica de tipos de datos replicados
title_full Especificación y semántica de tipos de datos replicados
title_fullStr Especificación y semántica de tipos de datos replicados
title_full_unstemmed Especificación y semántica de tipos de datos replicados
title_sort especificación y semántica de tipos de datos replicados
publisher Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
publishDate 2020
url https://hdl.handle.net/20.500.12110/tesis_n6778_Roldan
http://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesis&d=tesis_n6778_Roldan_oai
work_keys_str_mv AT roldanchristianhugo especificacionysemanticadetiposdedatosreplicados
AT roldanchristianhugo specificationandsemanticofreplicateddatatypes
_version_ 1766016025186271232
spelling I28-R145-tesis_n6778_Roldan_oai2023-04-26 Melgratti, Hernán Claudio Roldán, Christian Hugo 2020-03-20 La infraestructura para almacenes de datos replicados ofrece un throughput (o latencia) bajo y la capacidad de seguir respondiendo ante la presencia de fallas. Sin embargo, un resultado conocido por la sigla CAP [1] (Consistency, Availability y Partition Tolerance) establece que no es posible garantizar alta disponibilidad, tolerancia a fallas y consistencia (fuerte) simultáneamente. Como consecuencia, una de estas tres propiedades debe ser descartada. En la actualidad, muchas bases de datos replicadas, como Dynamo [2] o Cassandra [3] se construyen relajando la noción de consistencia y ofreciendo versiones más débiles de consistencia, conocidas generalmente como Consistencia Eventual [4]. La consistencia eventual garantiza que cualquier escritura será entregada a cada réplica del sistema y que tarde o temprano todas las réplicas convergerán a un mismo estado. Sin embargo, esto significa también, que (i) las réplicas mostrarán inconsistencia de datos (o anomalías) hasta que todas las réplicas lleguen al mismo estado y que (ii) todas las réplicas deben utilizar la misma política de resolución de conflictos ante la presencia de escrituras concurrentes con el fin de garantizar la convergencia. Las sistemas replicados adoptan diferentes estrategias para lidiar con inconsistencias temporales y resolver conflictos entre escrituras concurrentes, por ejemplo el uso de tipos de datos replicados (RDTs) [5, 6]. Por lo tanto, la solución seleccionada impacta en las propiedades aseguradas por el sistema, es decir, en el tipo de inconsistencias o anomalías que las aplicaciones permiten y observan. Dichas anomalías se caracterizan generalmente en términos de modelos de consistencia (como monotonic-read y consistencia causal) definidas axiomáticamente restringiendo las computaciones que pueden ocurrir en un sistema replicado [7, 8, 9]. Esta tesis contribuye al desarrollo de modelos de programación y técnicas de análisis para construir aplicaciones que lidien con nociones de consistencia débil. Presentamos una técnica de especificación para datos replicados cuya presentación será denotacional, para luego, movernos a una descripción categorial. Esta caracterización funcional es una propuesta alternativa a los enfoques operacionales actuales que se basan en historias abstractas [10, 11, 12, 13]. Brindamos, por lo tanto, una caracterización directa sobre la correctitud de las implementaciones de los RDTs basándonos en una relación de simulación entre los estados de una implementación concreta y los estados abstractos determinados por nuestra especificación [14]. Siguiendo el enfoque denotacional, asociamos a los tipos de datos replicados objetos matemáticos que representan su significado (es decir, definen dominios). En nuestra visión, estos objetos son funtores de PIDag(L) en SPath(L), donde PIDag(L) es la categoría de los Labelled Directed Acyclic Graphs (LDAGs) y morfismos que reflejan el pasado y SPath(L) es la categoría de conjuntos de caminos (u ordenes posibles sobre las operaciones) y morfismos entre conjuntos de caminos (que denota los ordenes admisibles). Damos una caracterización de tipos de datos replicados en término de las propiedades que los funtores gozan respecto de la flechas de PIDag(L) (por ejemplo, en término de la preservación de pullback/pushout). Como es usual con las semánticas funtoriales, la presentación categorial resultante de la actividad precedente posibilita el desarrollo de operadores adecuados para composición de especificaciones. Por último, estudiamos la semántica de programas corriendo sobre sistemas replicados, es decir, desarrollamos una caracterización alternativa para modelos de consistencia débil que son lo suficientemente general como para capturar algunos de los modelos de consistencia conocidos [15]. Mostramos algunas instanciaciones en nuestro framework y probaremos que las caracterizaciones obtenidas son sound y complete. Más aún, mostramos que a partir de este modelo se desprende una semántica denotacional de programas. Replicated data storages provide low throughput (or latency) and the ability to serve requests even in the presence of communication failures. However, the CAP Theorem [1] states that it is not possible to guarantee simultaneously high availability, fault tolerance and consistency (strong). Hence, one of these three properties must be discarded. Today’s popular data storages, such as Dynamo [2] or Cassandra [3] are built on the top of replicated data storage systems by relaxing consistency and offer weaker notions of consistency, called Eventual Consistency [4]. Roughly, eventual consistency guarantees that all updates will be delivered to the all the replicas, which will eventually converge to the same state. However that also means (i) replicas temporarily exhibit some discrepancies as long as they eventually converge to the same state, and (ii) all replicas have to use the same policy to solve conflict among concurrent updates in order to achieve the same state. Storages adopt different strategies to cope with temporary inconsistencies and to resolve conflicts among concurrent updates, such as Replicated data types (RDTs) [5, 6]. Therefore, the selected solution impacts on the properties ensured by a store, i.e., on the kind of inconsistencies or anomalies that are allowed to happened and observed by applications. Such anomalies are characterised in terms of consistency models (such as monotonic-read and causal consistency) defined axiomatically by constraining the performed computations from a data store [7, 8]. This thesis contributes to the development of programming models and analysis techniques suitable for the development of applications that rely on weak consistent, replicated stores. We develop a denotational specification technique for replicated data (such as counters, registers and sets), and then move to a categorical presentation. This functional characterisation is an abstract counterpart of the previuous operational approaches, which rely on abstract histories. Addiotionaly, we provide a direct characterisation of the correct implementations of RDTs in terms of a simulation relation between the states of a concrete implementation and the abstract ones determined by the specification [14]. Following the denotational approach, we associate the types of replicated data with mathematical objects that represent their meaning (that is, define domains). In our view, these objects are functors from PIDag(L) into SPath(L), where PIDag(L) is the category of Labelled Directed Acyclic Graphs (LDAGs) and morphisms that reflect the past and SPath(L) is the category of path-sets (or possible orders of operations) and morphisms between path-sets (denoting the admissible orders). We give a characterisation of replicated data types in terms of the properties that functors enjoy with respect to PIDag(L) (e.g., in terms of the preservation of pullback / pushout). As it is standard in classical results of functorial semantics, the categorical presentation will enable us to develop suitable operators for the composition of specifications. Finally, we study the semantics of programs running on replicated systems, i.e., we develop a parametric characterisation of weak consistent models general enough to capture well-known consistency models [15]. This allow us to prove the correctness of the programs working with different weak consistency models. We show some instantiation of this framework and prove that the obtained characterisations are sound and complete. Moreover we are able to obtain a denotational semantic of programs. Fil: Roldán, Christian Hugo. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. application/pdf https://hdl.handle.net/20.500.12110/tesis_n6778_Roldan spa Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar Especificación y semántica de tipos de datos replicados Specification and semantic of replicated data types info:eu-repo/semantics/doctoralThesis info:ar-repo/semantics/tesis doctoral info:eu-repo/semantics/publishedVersion http://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesis&d=tesis_n6778_Roldan_oai

Ejemplares similares