Relaxed Memory Models Seminar

Instructor: Viktor Vafeiadis

Teaching assistant:

Meeting time: 2 hours, once a week, April - July 2013

Abstract

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.

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

rmms (last edited 2013-03-04 14:08:02 by viktor)