The last decade has seen a dramatic growth in cloud-based Internet services. Websites such as Amazon and Facebook process hundreds of thousands of user requests per second, yet are available at all times. To achieve this, the shared data accessed by the requests is managed by novel cloud databases that partition and replicate the data across a large number of nodes and/or a wide geographic extent.

One of the main challenges faced by cloud databases is to maintain data consistency in the presence of a massive number of concurrent modifications on different nodes, despite the inevitable failures. The classic approach is for the database to make data distribution and parallel processing transparent to the application, i.e., to behave as if it were processing serial application requests on a single, unsplit copy of the data. This strong consistency model makes it easier for the programmer to build correct applications. Unfortunately, achieving this requires the various database nodes to synchronize, which undermines the benefits of parallelism.

This has motivated academia and industry to explore alternative architectures for cloud databases that relax the synchronization between their nodes. This enables high availability and low latency by allowing one database node to respond to a request without contacting the others. It also enables high scalability, as adding more nodes to the database translates into higher throughput. Finally, the relaxation of synchronization creates more parallelism and thus uses the available hardware more cost-effectively. However, there is a downside: databases that relax synchronization expose applications to the undesirable effects of parallelism. The resulting programming models are very difficult to use correctly, and we currently lack advanced methods and tools to help programmers in this task.

The goal of the RACCOON ERC project is to develop a synergy of novel reasoning methods, static analysis tools, and database implementation techniques that maximize the effects of cloud database parallelism while enabling application programmers to guarantee correctness. To this end, we first develop methods to formally reason about how weakening the consistency guarantees provided by cloud databases affects the correctness of the application and the parallelism allowed within the databases. This is based on techniques from programming languages and software verification. The resulting theory serves as the basis for practical implementation techniques and tools that take advantage of database parallelism, but only to the extent that its side effects do not affect applications.