Course pages 2017–18
Multicore Semantics and Programming
Slides for Part 1 (Peter Sewell)
- Slides for week 1 (introduction)
- Slides for weeks 1 and 2 (x86, architectures) (Peter Sewell)
- Slides for week 2 (testing)
- Slides for week 3 (ARM and POWER)
- Slides for week 4 (C/C++11): PL intro, C/C++11 intro (slides from Francesco Zappa Nardelli), and C/C++11 details (slides from Mark Batty).
Papers and tools
- ARM, Power and x86 model web interface: rmem
- diy7 tools for litmus testing
- Understanding POWER Multiprocessors. Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, Derek Williams. In PLDI 2011 (more details)
- Synchronising C/C++ and POWER. Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty, Peter Sewell, Luc Maranget, Jade Alglave, Derek Williams. In PLDI 2012. (more details)
- Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA. Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, Peter Sewell. In POPL 2016 (more details).
- Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8, Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell, July 2017. Draft. project page |
Code for C/C++11 stack example
Slides for Part 2 (Tim Harris)
- Slides for 3 Nov (locking) [PDF] [PPTX] (Tim Harris)
- MCS locks
- Cohort locks
- Flat combining
- Fine-grained loops using ideas from flat combining
- PGX project
- Slides for 17 Nov (lock-free programming) [PDF] [PPTX] (Tim Harris)
- Slides for 24 Nov (transactional memory) [PDF] [PPTX] (Tim Harris)
Example exercises
- There is an example exercise sheet and solution notes available for Tim Harris' section of the course. These are made available to provide an additional range of questions—there is no need to submit the answers.
Last year’s course materials are still available.