In this lecture, we will present selected design and implementation issues of microkernels with a focus on the L4 microkernel.

After motivating microkernels as the foundation of operating systems, we will cover L4's fundamental abstractions (threads and address spaces) and related topics such as kernel entry (syscall), thread switching, and kernel memory management. After that, we will present L4's inter-process communication (IPC) and memory mapping mechanisms, which allow manipulation of the previously discussed abstractions.

Additional topics outline some of the aspects relevant for implementing general purpose operating systems on top of L4: scheduling, hardware-dependent as well as -independent optimizations (small spaces, local IPC), and provisions for managing I/O devices at user-level. This outline is complemented by a discussion of security in a microkernel-based system, with a focus on controlling data flow (confidentiality).