Microkernel Construction Lecture Notes

Table of Contents

1. Overview
Monolithic Kernels
Microkernel-Based Systems
Historic Attempts
Basic Abstractions and Mechanisms
2. Threads and Thread Switching
Switching Threads
Kernel Stack Models
Per-Processor Kernel Stack
Per-Thread Kernel Stack
Sample Code
3. System Calls
Traditional System Calls on x86
Fast System Calls on x86
Reconciling Stack Layouts
Returning From System Calls
4. TCBs
Locating TCBs
Locating the TCB of the Current Thread
Locating the TCB of a Thread by Thread ID
Locating the TCB of the Next Ready-to-Run Thread
Address Space Layout
Address Space Regions
Regions in the Kernel Address Space
Synchronization of the Kernel Address Space
Processor-Specific Data
5. IPC Functionality and Interface
Synchronous Communication
Communication Primitives
Message Types
Send Timeout
Receive Timeout
Transfer Timeout
Timeout Encoding
Encoding of IPC Parameters
Operation and Addresses
Deceiving IPC and Proxies
Message Content
Receive Buffers
IPC Result
Virtual Registers and the UTCB
6. IPC Implementation
IPC and Scheduling
General Implementation of Short IPC
Fast Path IPC
Performance Considerations
Combining Fast and Slow Paths
Long IPC
String IPC
Copy In/Copy Out
Temporary Mapping Area
Management of the Temporary Mapping Area
Temporary Mapping Area on Multi-Processor Machines
7. Dispatching
Scheduling in L4
Dispatching Mechanism
Lazy Dispatching
8. Virtual Memory Mapping
9. Small Spaces
10. Local IPC
11. Interrupt and Exception Handling
12. Security
A. Communication Spaces