La última década ha sido testigo de un crecimiento espectacular de los servicios de Internet basados en la nube. Sitios web como Amazon y Facebook procesan cientos de miles de peticiones de los usuarios por segundo, y aún así están disponibles en todo momento. Para conseguirlo, los datos compartidos a los que acceden las peticiones se gestionan mediante novedosas bases de datos en la nube que particionan y replican los datos en un gran número de nodos y/o una amplia extensión geográfica.
Uno de los principales retos a los que tienen que hacer frente las bases de datos en la nube es mantener la coherencia de los datos en presencia de un número masivo de modificaciones concurrentes en diferentes nodos, a pesar de los inevitables fallos. El enfoque clásico es que la base de datos haga que la distribución de datos y el procesamiento paralelo sean transparentes para la aplicación, es decir, que se comporte como si procesara las solicitudes de la aplicación en serie en una única copia no dividida de los datos. Este modelo de consistencia fuerte facilita al programador la construcción de aplicaciones correctas. Desgraciadamente, para conseguirlo es necesario que los distintos nodos de la base de datos se sincronicen, lo que socava las ventajas del paralelismo.
Esto ha motivado al mundo académico y a la industria a explorar arquitecturas alternativas para las bases de datos en la nube que relajan la sincronización entre sus nodos. Esto permite una alta disponibilidad y una baja latencia, al permitir que un nodo de la base de datos responda a una petición sin ponerse en contacto con los demás. También permite una alta escalabilidad, ya que añadir más nodos a la base de datos se traduce en un mayor rendimiento. Por último, la relajación de la sincronización crea más paralelismo y, por tanto, utiliza el hardware disponible de forma más rentable. Sin embargo, hay un inconveniente: las bases de datos que relajan la sincronización exponen a las aplicaciones a los efectos indeseables del paralelismo. Los modelos de programación resultantes son muy difíciles de utilizar correctamente, y actualmente no disponemos de métodos y herramientas avanzadas que ayuden a los programadores en esta tarea.
El objetivo del proyecto RACCOON ERC es desarrollar una sinergia de métodos de razonamiento novedosos, herramientas de análisis estático y técnicas de implementación de bases de datos que maximicen los efectos del paralelismo de bases de datos en la nube, al tiempo que permite a los programadores de aplicaciones garantizar la corrección. Para ello, primero desarrollamos métodos para razonar formalmente sobre cómo el debilitamiento de las garantías de consistencia proporcionadas por las bases de datos en la nube afecta a la corrección de la aplicación y al paralelismo permitido dentro de las bases de datos. Esto se basa en técnicas de los lenguajes de programación y la verificación de software. La teoría resultante sirve de base para las técnicas y herramientas de implementación práctica que aprovechan el paralelismo de las bases de datos, pero sólo en la medida en que sus efectos colaterales no afecten a las aplicaciones.
