What is weak memory consistency?
Weak memory consistency is the formal study of the exact behaviours
concurrent programs can exhibit. (Naively, one might think that all the
behaviours of a multithreaded program can be generated by some arbitrary
interleaving of its threads. This assumption, however, is incorrect. Due to
compiler and/or hardware optimizations, concurrent programs can exhibit a
number of additional "weak" behaviours.)
What will the seminar cover?
It will cover the key topics in the field:
- Semantics of concurrent programs on modern architectures (x86, Arm)
- Concurrency semantics of C/C++ and other imperative programming languages
- Semantics of programs writing to persistent storage (e.g., non-volatile memory)
- Correctness of compiler optimizations on concurrent programs
- The data-race-freedom theorem
- Verification of weakly consistent concurrent programs
Lectures