Título: Verificación de correctitud para tipos de datos replicados en Coq
Directores: Christian Roldán y Hernán Melgratti
Jurados: Fernando Asteasuain y Agustín Martinez Suñé

Resumen:

La replicacion de datos es un concepto fundamental en sistemas distribuidos ya que ofrece garantías como escalabilidad y alta disponibilidad a expensas de tener una vision inconsistente del estado del sistema. Esto significa que los usuarios de dicho sistema, temporalmente, podrían percibir diferencias sobre el estado del mismo.

En particular, esta tesis se concentra en un enfoque de replicación basada en estados, donde cada réplica (o nodo) que compone al sistema, transmite su estado al resto de las réplicas con el fin que estas puedan combinarlo con su propio estado y alcancen así un mismo estado común. La literatura propone los tipos de datos replicados o RDTs (por su acrónimo en inglés, Replicated Data Types) quienes lidean con inconsistencias temporales que puedan existir y resuelven de forma automática cuando existen conflictos entre escrituras concurrentes. Diferentes líneas de investigación han abordado el problema de especificar e implementar RDTs. Más aún, hay demostraciones manuales sobre la correcta implementación de un RDT con respecto a su especificación.

En esta tesis proponemos abordar el problema de formalizar y verificar la correcta implementación de RDTs utilizando el asistente de demostraciones Coq. Coq es un sistema formal de semidesición de manejo de demostraciones de teoremas chequeadas por computadora. Proveemos por lo tanto, de un marco de trabajo para verificar la correctitud de RDTs de una manera computarizada, lo cual ofrece una alternativa confiable y mecánica de abordar esta tarea. Mas concretamente, en esta tesis nos centramos en realizar la experiencia de formalizar en Coq una especificacion y una implementacion de un RDT (tomando como caso de estudio el tipo de datos: Contador). Para esto, (i) mostraremos como transformar las definiciones existentes en definiciones equivalentes en Coq. Luego, (ii) probaremos que la implementacion del tipo de datos es correcta, basándonos en un resultado que establece la existencia de una relacion de simulacion entre la semantica operacional asociada a la especificacion, y la implementacion concreta del Contador. Finalmente, (iii) presentamos una prueba en el asistente sobre la correcta implementación del tipo de datos, mostrando para esto, la existencia de dicha relación de simulación.