Revision 1 as of 2013-01-24 14:00:52
|Deletions are marked like this.||Additions are marked like this.|
|Line 16:||Line 16:|
== Preliminary syllabus ==
1. Introduction and basic concepts
2. Java memory model: what went wrong?
3. The SPARC/x86 TSO model
4. Data race freedom theorems about TSO
5. TSO variants: PSO, RMO, TLO, PLO
6. Verification results on TSO, PSO, RMO
7. TSO-preserving compilation
8. Power/ARM model
9. DRF models: C/C++11 model
10. Compilation from C++ to x86 and Power
11. Reasoning about C++ programs
Relaxed Memory Models Seminar
Instructor: Viktor Vafeiadis
Meeting time: 2 hours, once a week, April - July 2013
Whether we like it or not, concurrent programming is essential for achieving high performance on modern hardware. Multiprocessors provide a shared memory model, where all threads of execution have access to the same memory locations, but where the exact semantics of concurrent access differs from one processor to another. The precise semantics of concurrent access to shared locations guaranteed by a processor architecture or a programming language definition is called the memory model.
This course will study such memory models for architectures such as x86, SPARC, and Power, and for programming languages, such as C/C++ and Java.
The course is being taught by Viktor Vafeiadis (MPI-SWS, the Kaiserslautern branch) and will be conducted by videoconferencing between the two MPI-SWS locations.
- Introduction and basic concepts
- Java memory model: what went wrong?
- The SPARC/x86 TSO model
- Data race freedom theorems about TSO
- TSO variants: PSO, RMO, TLO, PLO
- Verification results on TSO, PSO, RMO
- TSO-preserving compilation
- Power/ARM model
- DRF models: C/C++11 model
- Compilation from C++ to x86 and Power
- Reasoning about C++ programs