# Programming Languages and Tools Lab

## Summer School on Weak Memory Consistency

**Instructors:** Viktor Vafeiadis, Ori Lahav, The Max Planck Institute for Software Systems, Germany.

### General Information

The school will be carried out in English, attendance is free of charge, but the number of participants is potentially limited. The exact time and venue will be announced later.

To register for the school and receive future announces please join the following group:

https://groups.google.com/forum/#!forum/jbr_summer...

### Synopsis

Many programmers naively assume that all the behaviours of a concurrent program can be generated by some arbitrary interleaving of its threads. This assumption, however, is incorrect. Due to compiler and/or hardware optimisations, concurrent programs can exhibit a number of behaviours that are not explainable by any interleaving of their threads. The formal study of the exact behaviours concurrent programs can exhibit is a field known as*weak memory consistency*.

This course will cover the key results in this field, starting with the formal definitions of some important weak memory models, and moving to establishing basic results about them, such as the DRF theorem, and proving the correctness of program transformations within a model or compilation from one model to another. The course will also contain some recent research outcomes, and finish with a set of open research questions. In more detail, the course will cover the following topics:

- Operational memory models:
- Sequential consistency (SC)
- Total store order (TSO)
- Partial store order (PSO)
- Release-acquire (RA)

- Axiomatic memory models:
- Basic models: SC, TSO, RA, Coherence
- Comparing axiomatic memory models
- The OOTA problem

- Fundamental results about memory models:
- The DRF theorem
- Correctness of program transformations
- Relating operational and axiomatic models

- Resolving the OOTA problem
- Promising semantics
- Event structure semantics

- Verification of programs under weak memory consistency
- Relaxed separation logic
- Model checking

In addition to the lectures, there will be example classes demonstrating some of the existing tools for working with weak memory models.

### Slides

- Day 1. Introduction to weak memory consistency
- Day 1. Basic operational semantics for concurrency
- Day 1. Declarative semantics for concurrency
- Day 2. Correspondence between operational and declarative concurrency semantics
- Day 2. Correctness of compilation under weak memory models
- Day 3. Correctness of compiler optimizations
- Day 3. Model checking for weak memory models
- Day 3. The C11 memory model
- Day 4. The DRF theorem
- Day 4. Reduction from RA to SC using fences
- Day 4. OGRA: Owicki-Gries for RA
- Day 4. The OOTA problem and a promising solution
- Day 5. Concurrent separation logic
- Day 5. Relaxed separation logic