Registro:
| Documento: | Tesis Doctoral |
| Título: | Especificación y semántica de tipos de datos replicados |
| Título alternativo: | Specification and semantic of replicated data types |
| Autor: | Roldán, Christian Hugo |
| Editor: | Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales |
| Publicación en la Web: | 2022-03-29 |
| Fecha de defensa: | 2020-03-20 |
| Fecha en portada: | 2020-11 |
| Grado Obtenido: | Doctorado |
| Título Obtenido: | Doctor de la Universidad de Buenos Aires en el área de Ciencias de la Computación |
| Director: | Melgratti, Hernán Claudio |
| Consejero: | Braberman, Víctor Adrián |
| Jurado: | D'Argenio, Pedro R.; Jaskielof, Mauro; Bonelli, Eduardo |
| Idioma: | Español |
| Formato: | PDF |
| Handle: |
http://hdl.handle.net/20.500.12110/tesis_n6778_Roldan |
| PDF: | https://bibliotecadigital.exactas.uba.ar/download/tesis/tesis_n6778_Roldan.pdf |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/tesis/document/tesis_n6778_Roldan |
| Ubicación: | Dep.COM 006778 |
| Derechos de Acceso: | Esta obra puede ser leída, grabada y utilizada con fines de estudio, investigación y docencia. Es necesario el reconocimiento de autoría mediante la cita correspondiente. Roldán, Christian Hugo. (2020). Especificación y semántica de tipos de datos replicados. (Tesis Doctoral. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de http://hdl.handle.net/20.500.12110/tesis_n6778_Roldan |
Resumen:
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.
Abstract:
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.
Citación:
---------- APA ----------
Roldán, Christian Hugo. (2020). Especificación y semántica de tipos de datos replicados. (Tesis Doctoral. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/tesis_n6778_Roldan
---------- CHICAGO ----------
Roldán, Christian Hugo. "Especificación y semántica de tipos de datos replicados". Tesis Doctoral, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2020.https://hdl.handle.net/20.500.12110/tesis_n6778_Roldan
Estadísticas:
Descargas totales desde :
Descargas mensuales
https://bibliotecadigital.exactas.uba.ar/download/tesis/tesis_n6778_Roldan.pdf
