Seminar Computer Science - Prof. dr. R. Meyer

Title: Replication and Consistency

Abstract:
Parallel programming needs efficient access to shared data. Efficient access to data, in turn, needs physical proximity - the closer the data the faster the access. A key question of parallel programming is therefore how to bring a
single datum close to different compute units. The answer, given uniformly across all layers of abstraction, is replication: by creating a copy of the datum for every compute unit. Replication occurs in various forms.
In hardware architectures, processes use caches to reduce the latency of memory accesses. In programming languages, branch prediction is used to fill registers. In concurrency libraries, threads have different views of the shared heap.
In geo-replicated databases, storage centers hold copies of the same datum.

Once replicated, the question is how to update a datum. Of course, each compute unit will update its own replica. But when do the other compute units learn about the modification? The answer, given uniformly across all layers of abstraction, is:
sometime later. When, depends on the communication mechanism of the execution environment.

While updates travel from one compute unit to the other, the corresponding replicas hold inconsistent values. As much as efficiency is the blessing brought by replication, inconsistency is the curse. Programming in the presence of inconsistency is plain difficult, even for experts. Besides the interleavings brought by parallel processing, the programmer has to keep in mind the communication among replicas.

Over the past ten years, we have developed algorithms that make it easier for the programmer to work with data replication. The contributions range from compiler technology that hides the effects of the hardware architecture over type systems that guarantee proper synchronization in concurrent data structures to verification technology that takes into account a description of the execution environment.
We use techniques from automata theory, concurrency theory, logic, programming languages, and verification.

In this talk, I will give an introduction to replication and consistency and then elaborate on the former two projects.
The results are joint work with Ahmed Bouajjani, Egor Derevenetc, and Sebastian Wolff. They have been published at [ICAP'11,ESOP'13, ICALP'14, POPL'19, POPL'20].