Lectures

Times and locations

Day Weeks Start End Location
Wednesay 1–5, 7–10 9:00 11:00 Webster Theatre B (K-G15-290) & Online
Thursday 1–5, 7–10 16:00 18:00 Webster Theatre A (K-G15-190) & Online

Slides and Video

Week Day Lecturer Topic Video Slides
1 Wed Gernot Introduction (Microkernels and seL4) PDF slides
1 Thu Gernot seL4 API and usage PDF
2 Wed Kevin OS Execution Models PDF
2 Thu 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]
PDF
PDF
3 Wed Gernot Caches (What every OS designer must know)
Papers: [Clark & Emer 1985], [Uhlig et al., 1994], [Wiggins, 2003]
Book: [Schimmel, 1994]
PDF
3 Thu Gernot Virtual Machines (Introduction and principles)
Papers: [Barham et al., 2003], [Waldspurger, 2002]
PDF
4 Wed Gernot Performance Measurement and Analysis
Paper: [Fleming & Wallace, 1986]
Other: [Gernot's List of Benchmarking Crimes]
4 Thu Gernot Real-Time Systems Introduction
Book: [Liu, 2000]
Papers: [Lyons et al., 2018]
5 Wed Peter Unix and Linux Internals
Papers: [McKenney, 2004], [McKenney et al 2009], [Ritchie & Thompson, 1974]
5 Thu Gernot Microkernel Design and Implementation (with focus on seL4)
Papers: [Liedtke, 1993], [Liedtke, 1995], [Blackham et al., 2012], [Heiser & Elphinstone, 2016]
6 Wed – – Flex week – no lecture – – – –
6 Thu – – Flex week – no lecture – – – –
7 Wed Gernot Security Fundamentals
Reference: [Miller et al., 2003]
7 Thu Gernot Information Leakage
(timing channels and speculation)
Papers: [Liu et al., 2015], [Lipp et al., 2018], [Kocher et al., 2019]
8 Wed Kevin SMP and Locking 1
8 Thu Kevin SMP and Locking 2
9 Wed Ihor Multicore Operating Systems Pt 1
9 Thu Ihor Multicore Operating Systems Pt 2
10 Wed Gernot Formal Verification and seL4
10 Thu Gernot Local OS Research (1h)
Having fun with seL4 and beyond
10 Thu Gernot Exam preparation (1h) – –
The schedule for future lectures is tentative and subject to change!

References in square brackets are recommended readings from the papers list.

The icon for the video indicates accessibility:
UNSW only accessible to UNSW staff and students
public YouTube freely accessible on the UNSW CSeLearning COMP9242 YouTube channel