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
- Verification of programs under weak memory consistency
- Relaxed separation logic
- Model checking
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