Título: «Una caracterización operacional para modelos de consistencia transaccional»

Jurados: Hernán Melgratti,  Agustín Martinez Suñé

Director: Christian Roldán

La misma será transmitida al público general a través del siguiente link:

• Link Aula Zoom: https://zoom.us/my/dc.aula09
• Nombre Aula Zoom: dc.aula09
• Clave del Aula Zoom: H.Lamarr

Solicitamos que por favor al conectarse silencien sus micrófonos.

Resumen:

Hoy en día se construyen aplicaciones sobre bases de datos replicadas que garantizan escalabilidad y alta disponibilidad a expensas de sacrificar la consistencia, es decir, los usuarios pueden observar temporalmente diferencias sobre el estado del sistema. Un modelo de consistencia caracteriza este tipo de inconsistencias o anomalías. Por lo tanto, razonar sobre la semántica de programas está directamente ligado a los modelos de consistencia que este tipo de bases de datos ofrecen. La literatura define a los modelos de consistencia en términos de axiomas que restringen las posibles ejecuciones en una base de datos replicada. En particular, en esta tesis nos concentramos en modelos de consistencia para transacciones. Una traza de ejecución es reconstruida a través de un grafo de eventos conocido como ejecución abstracta. La misma se define sobre un conjunto de transacciones y dos relaciones: (i) visibilidad, que define cuando una transacción es conocida por otra, y (ii) arbitración, que especifica un orden relativo entre las transacciones ejecutadas por el sistema. Estos mecanismos, si bien son declarativos, no inducen una operatoria clara que pueda ser sencillamente traducida a una implementación.

En esta tesis desarrollamos un modelo operacional basado en un sistema de transición etiquetado que captura de forma general los modelos de consistencia para transacciones. Para esto definimos el estado del sistema como un orden parcial sobre una secuencia de transacciones. Además proponemos una regla de equivalencia estructural, y un conjunto de reglas de derivación descriptas en términos de dos predicados paramétricos: commit consistency y arbitration consistency. Cada modelo de consistencia transaccional, como Snapshot Isolation y Causal Consistency, es presentado a partir de la instanciación de cada predicado, ofreciendo así, definiciones alternativas de los mismos. Probaremos entonces, la equivalencia entre la presentación clásica para modelos de consistencia transaccional, que son definidas axiomáticamente, y nuestro modelo operacional. Concretamente, demostramos la correspondencia de ambos enfoques presentando pruebas de soundness y completeness para cada modelo.