Replication and Consistency

Organization

Instructor: Dr. Annette Bieniusa

The lecture and course material will be in English.

Please register for the course in Olat!

Prerequisites:

  • Good programming knowledge in Java or C/C++

As this is a 4-CP lecture, you will spend on average around 120 hours on the lecture and the exercises, including exam preparation. If you do not have much experience with programming systems of medium size and moderate complexity, you need to plan to spend more time on the practical exercises. If you lack some of the theoretical prerequisites (definition of formal languages, finite-state machines, proof techniques), you should also include revisions for these topics into your planning.

Objectives

You will be able to

  • understand and explain the underlying mechanisms of classical concurrent and replicated data structures,
  • explain and elaborate the limitations of non-blocking synchronization mechanisms, and
  • formally describe and compare standard memory and consistency models for concurrent systems.

Topics of the Lecture

  • Basic notions
    • Happens-Before relation
    • Histories and abstract executions
    • Sequential consistency and linearizability
    • Compositionality
  • Non-blocking synchronisation in shared-memory architectures
    • Primitive synchronization operations
    • ABA problem
    • Concurrent lists, queues and stacks
  • Memory models
    • Total-Store-Order (TSO)
    • Axiomatic formal models
    • Data Race freedom
    • Robustness