L4 Essentials

Basic concepts of threads and address spaces. Kernel provides IPC.

Supports recursive address spaces. Have user-level pagers that use kernel services of granting, mapping and unmapping portions of an address space. Page faults go to the appropriate pager.

I/O ports are mapped to address space for user-level device-drivers.

Hardware interrupts handled by IPC.

Use Pentium-specific optimization for address spaces of 4MB to 512MB (total of all spaces is 512MB). Allows simulation of a tagged TLB.

Question: How much of later benchmarking uses this optimization?

Also L4 versions for Alpha and MIPS architectures.