Course pages 2012–13
Multicore Semantics and Programming
Principal lecturers: Dr Peter Sewell, Dr Timothy Harris
Taken by: MPhil ACS, Part III
Hours: 16 (8 × two-hour blocks, including 2 × one-hour practical sessions)
Prerequisites: Some familiarity with discrete mathematics (sets, partial orders, etc.) and with sequential Java programming will be assumed. Experience with operational semantics and with some concurrent programming would be helpful.
In recent years multiprocessors have become ubiquitous, but building reliable concurrent systems with good performance remains very challenging. The aim of this module is to introduce some of the theory and the practice of concurrent programming, from hardware memory models and the design of high- level programming languages to the correctness and performance properties of concurrent algorithms.
Part 1: Introduction and relaxed-memory concurrency (Peter Sewell)
- Introduction. Sequential consistency, atomicity, basic concurrent problems. [1 block]
- Concurrency on real multiprocessors: the relaxed memory model(s) for x86, and theoretical tools for reasoning about x86-TSO programs. Other hardware models for contrast: Power/ARM/Itanium. [2 blocks]
- High-level languages. An introduction to Java and C++0x shared- memory concurrency, including the basic Java concurrency primitives and some discussion of Java memory models and compiler optimisations. [1 block]
Part 2: Concurrent algorithms (Tim Harris)
- Concurrent programming. Simple algorithms (readers/writers, stacks, queues) and correctness criteria (linearisability and progress properties). Advanced synchronisation patterns (e.g. some of the following: optimistic and lazy list algorithms, hash tables, double-checked locking, RCU, hazard pointers), with discussion of performance and on the interaction between algorithm design and the underlying relaxed memory models. [3 blocks, including two 1-hour practical sessions]
- Research topics, likely to include one hour on transactional memory and one guest lecture. [1 block]
On completion of this module, students should:
- have a good understanding of the semantics of concurrent programs, both at the multprocessor level and the C/Java programming language level;
- have a good understanding of some key concurrent algorithms, with practical experience.
Coursework will consist of assessed exercises.
There will be two 1-hour practical sessions, as above.
The assessment will be based on assessed coursework exercises (75%) and practical reports (25%).
Herlihy, M. & Shavit, N. (2008). The art of multiprocessor programming. Morgan Kaufmann.