Microkernel Construction

Links

Contents

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).

Literature

J. LeVasseur: IA32 Condensed for Kernel Developers
System Architecture Group (updated on May 3, 2006)
J. Liedtke et al.: The Performance of µ-Kernel-Based Systems
Proceedings of the 16th ACM Symposium on Operating System Principles (SOSP), St. Malo, France, October 1997
J. Liedtke: On µ-Kernel Construction
Proceedings of the 15th ACM Symposium on Operating System Principles (SOSP), Copper Mountain Resort, CO, December 1995
J. Liedtke: Improving IPC by Kernel Design
Proceedings of the 14th ACM Symposium on Operating System Principles (SOSP), Asheville, NC, December 1993
J. Liedtke: Toward Real µ-kernels
Communications of the ACM, 39(9), pp. 70-77, September 1996
J. Liedtke et al.: The SawMill Framework for Virtual Memory Diversity
Proceedings of the 6th Australasian Computer Systems Architecture Conference (ACSAC 2001), Bond University, Gold Coast, Queensland, January 29 - February 2, 2001
J. Liedtke: Clans & Chiefs
In 12. GI/ITG-Fachtagung Architektur von Rechensystemen, Springer Verlag, 1992
F. Hupfeld: Summary of the lecture "Construction of Microkernels" of Prof. J. Liedtke in summer term 2000
 
Intel Corporation: Intel® 64 and IA-32 Architectures Software Developer's Manual, Volume 1: Basic Architecture
Intel Corporation: Intel® 64 and IA-32 Architectures Software Developer's Manual, Volume 2A: Instruction Set Reference, A-M
Intel Corporation: Intel® 64 and IA-32 Architectures Software Developer's Manual, Volume 2B: Instruction Set Reference, N-Z
Intel Corporation: Intel® 64 and IA-32 Architectures Software Developer's Manual, Volume 3A: System Programming Guide, Part 1
Intel Corporation: Intel® 64 and IA-32 Architectures Software Developer's Manual, Volume 3B: System Programming Guide, Part 2