Chapter | Title | Recommended reading |
0 |
Prefix by Robert Kaiser, HSRM
(slides)
(audio)
(video)
|
|
1 |
Introduction (Microkernels and seL4) by Gernot Heiser, UNSW
(slides)
(handout)
(audio)
(video)
|
|
2 |
seL4 API and Usage by Gernot Heiser, UNSW
(slides)
(handout)
(audio)
(video)
|
|
3 |
OS execution models by Kevin Elphinstone, UNSW
(slides)
(handout)
(audio)
(video)
Why threads are a bad idea (for most purposes) by John Ousterhout, Sun Microsystems Labs
(slides)
(handout)
(audio)
(video)
Why events are a bad idea (for high-concurrency servers) by Rob von Behren et al, UCB
(slides)
(handout)
(audio)
(video)
|
[von Behren et al., 2003] |
4 |
Caches (What every OS designer must know) by Gernot Heiser, UNSW
(slides)
(handout)
(audio)
|
(video)
[Clark, Emer 1985]
[Uhlig et al. 1994]
[Wiggins 2003]
[Schimmel 1994]
|
5 |
Virtual Machines by Gernot Heiser, UNSW
(slides)
(handout)
(audio)
|
(video)
[Barham et al., 2003]
[Waldspurger, 2002]
[Dall and Nieh, 2013]
|
6 |
Performance Measurement and Analysis by Gernot Heiser, UNSW
(slides)
(handout)
(audio)
|
(video)
[Fleming and Wallace, 1986]
[Gernot's Benchmarking Crimes]
|
7 |
Real-Time Systems Introduction by Gernot Heiser, UNSW
(slides)
(handout)
(audio)
|
(video)
[Liu, 2000]
[Lyons et al., 2018]
|
8 |
Microkernel Design and Implementation (with focus on seL4) by Gernot Heiser, UNSW
(slides)
(handout)
(audio)
|
(video)
[Liedtke 1993]
[Liedtke 1995]
[Blackham et al. 2012]
[Heiser & Elphinstone 2016]
|
9 |
Security Fundamentals by Toby Murray and Gernot Heiser, UNSW
(slides)
(handout)
(audio)
|
[Miller et al, 2003]
|
10 |
Information Leakage (timing channels and speculation) by Gernot Heiser, UNSW
(slides)
(handout)
(audio)
|
[Liu et al., 2015]
[Lipp et al., 2018]
[Kocher et al., 2019]
|
11 |
Formal Verification and seL4 by Gernot Heiser, UNSW
(slides)
(handout)
(audio)
|
[Klein et al., 2014]
[Heiser 2020]
|
12 |
UNIX and Linux Internals by Peter Chubb, DATA61
(slides)
(handout)
(audio)
|
[McKenney, 2004]
[McKenney et al., 2002]
[Ritchie and Thompson, 1974]
|
13 |
SMP and Locking 1 by Kevin Elphinstone, UNSW
(slides)
(handout)
(audio)
|
[Anderson, 1990]
[Clements et al., 2013]
|
14 |
SMP and Locking 2 by Kevin Elphinstone, UNSW
(slides)
(handout)
(audio)
|
|
15 |
Multicore Operating Systems by Ihor Kuz, UNSW
(slides)
(handout)
(audio)
|
|
16 |
Local OS Research (Having fun with seL4 and beyond) by Gernot Heiser, UNSW
(slides)
(handout)
(audio)
|
[Biggs et al., 2018]
[Amani et al., 2016]
[Ge et al., 2019]
[Shen et al., 2019]
[Klein et al., 2018]
|