Lectures
Times and locations
| Day | Weeks | Start | End | Location |
|---|---|---|---|---|
| Monday | 1–3,5,7–10 | 16:00 | 18:00 | H13 Lawrence Theatre (K-H13-G001) |
| Wednesday | 1–5,7–10 | 16:00 | 18:00 | Ainsworth 202 (K-J17-202) |
Slides and Video
| Week | Day | Lecturer | Topic | Video | Slides |
|---|---|---|---|---|---|
| 1 | Mon | Gernot |
Introduction
(Microkernels and seL4) Apologies for the green screen in the video! |
|
|
| 1 | Wed | Gernot | seL4 API and usage |
|
|
| 2 | Mon | Kevin | OS Execution Models |
|
|
| 2 | Wed | Kevin |
Why Threads are a Bad Idea
(for most purposes)
Why Events are a Bad Idea (for high-concurrency servers) Paper: [von Behren et al., 2003] |
|
|
| 3 | Mon | Gernot |
Hardware considerations – Caches and Devices (What every OS designer must know) |
|
|
| 3 | Wed | Gernot |
Virtual Machines
(Introduction and principles) Papers: [Barham et al., 2003], [Waldspurger, 2002] |
|
|
| 4 | Mon | – – | Labour Day | – – | – – |
| 4 | Wed | Gernot |
Performance Measurement and Analysis Paper: [Fleming & Wallace, 1986] Other: [Gernot's List of Benchmarking Crimes] |
|
|
| 5 | Mon | Gernot |
Microkernel Design and Implementation
(with focus on seL4) Papers: [Liedtke, 1993], [Liedtke, 1995], [Heiser & Elphinstone, 2016] |
|
|
| 5 | Wed | Gernot |
Security Fundamentals References: [Miller et al., 2003] [Jaeger, 2008] [Bos, 2019] |
|
|
| 6 | Mon | – – | Flex week – no lecture | – – | – – |
| 6 | Wed | – – | Flex week – no lecture | – – | – – |
| 7 | Mon | Anna |
Real-Time Systems Introduction Book: [Liu, 2000] Papers: [Lyons et al., 2018] |
|
|
| 7 | Wed | Kevin |
SMP and Locking 1 Papers: [Anderson, 1990], [Clements et al. 2013] |
|
|
| 8 | Mon | Peter |
Unix and Linux Internals Papers: [McKenney, 2004], [McKenney et al 2009], [Ritchie & Thompson, 1974] |
|
|
| 8 | Wed | Gernot |
Formal verification and seL4 Papers: [Klein et al., 2014], [Sewell et al., 2017], [Blackham et al., 2012], [Heiser 2020], [Biggs et al., 2018] |
|
|
| 9 | Mon | Ihor |
Multicore Operating Systems Part 1 |
|
|
| 9 | Wed | Curtis | User-level synchronisation primitives |
|
|
| 10 | Mon | Ihor |
Multicore Operating Systems Part 2 |
|
|
| 10 | Wed | Kevin | SMP and Locking 2 |
|
|
| 11 | Wed | Gernot |
seL4 in the real world seL4-related research at UNSW [Klein et al., 2018], [Ge et al., 2019] |
|
|
| 11 | Wed | Gernot | Exam preparation (0.5h) | – – | – – |
References in square brackets are recommended readings from the papers list.
| The icon for the video indicates accessibility: | |
|---|---|
|
publicly accessible |