This post came to be as part of my LLM-assisted research, text here is wholly generated by Fable 5.1 model. All such posts are tagged with llm-gen so you can easily spot them. The summary is quite educational however, so I decided to publish it.
Distinction between process and event kernels
- Process kernel: every user thread has its own kernel stack. When a thread traps into the kernel (syscall, page fault, interrupt), the kernel runs "on behalf of" that thread, on that thread's kernel stack. If the kernel needs to wait for something (disk I/O, a lock), it can just block mid-syscall β the thread's kernel state lives on its stack, and the scheduler switches to another thread's kernel stack. Linux, Windows, the BSDs, and Fuchsia all work this way.
- Event (interrupt) kernel: there's one kernel stack per CPU, period. Every trap is treated as an event: the kernel runs a handler from start to finish, updates data structures, picks a thread to resume, and unwinds the stack back to empty. The kernel never blocks. If a thread needs to wait, the kernel marks it as waiting in a thread control block and returns β nothing about the operation is "kept on a stack". seL4, early L4 variants, and many RTOS kernels work this way.
| Process kernel | Event (interrupt) kernel | |
|---|---|---|
| Memory | A kernel stack per thread (Linux: 16 KB each) | One stack per CPU β tiny |
| Kernel code | Natural, sequential; can block anywhere | Every wait must be a explicit state machine |
| Preemption in kernel | Easy β just switch stacks | Hard; typically kernel runs to completion with interrupts off |
| Latency | Long syscalls can be preempted | Kernel paths must be short and bounded |
| Verification / reasoning | Many interleaved kernel stacks = hard to reason about | Kernel is atomic, run-to-completion: much easier to prove correct (this is why seL4 chose it) |
| Cache/TLB behaviour | Stack switching pollutes caches | Very cache-friendly |
- a process kernel makes the kernel code easy to write at the cost of more memory and more complex concurrency inside the kernel;
- an event kernel makes the kernel small, fast, and formally tractable at the cost of forcing every long operation to be written as an explicit continuation β which is why event kernels are almost always microkernels that push the "long" work (drivers, filesystems) out to user space.
