Table of Contents

Preface

1. Overview

Monolithic Kernels

Microkernel-Based Systems

Historic Attempts

Basic Abstractions and Mechanisms

2. Threads and Thread Switching

Threads

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

0-Mapping-Trick

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

Timeouts

Send Timeout

Receive Timeout

Transfer Timeout

Timeout Encoding

Encoding of IPC Parameters

Operation and Addresses

Deceiving IPC and Proxies

Timeouts

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

Optimizations

Dispatching Mechanism

Lazy Dispatching

Timeouts

8. Virtual Memory Mapping

9. Small Spaces

10. Local IPC

11. Interrupt and Exception Handling

12. Security

Index

A. Communication Spaces