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.

Event kernels

The constraint that shapes everything: the kernel can never block, so any operation that can't finish "now" has to be representable as a small, fixed-size piece of state in a kernel object. Every good event-kernel API decision is some consequence of that. Here are the considerations, each paired with a real design that gets it right (and one that got it wrong).

1. Every wait point must be a first-class kernel object

In a process kernel, "waiting" is implicit — the stack just sits there. In an event kernel the API must expose what you're waiting on as an object the kernel can record a pointer to in your TCB.

seL4 does this well: the only things a thread can block on are an Endpoint (synchronous IPC) or a Notification (asynchronous signal). A TCB in state BlockedOnReceive holds exactly one endpoint pointer plus a queue link. That's the entire continuation.

TCB
├─ state: BlockedOnReceive
├─ waiting_on: -> Endpoint #7
└─ queue_link ──> (next waiter)

What makes it good: the kernel never has to reconstruct what a thread was doing. It just looks at the object and the state enum. Compare Linux, where a thread's kernel stack may be 12 frames deep inside a filesystem when it blocks.

2. Payloads must be bounded and page-fault-free

If the kernel copies a message and the copy page-faults, the kernel now has to block mid-operation — which an event kernel can't do. So message size and location must be controlled.

L4 got this wrong first, then right. Original L4 had "long IPC": arbitrary-length copies between address spaces. Page faults during the copy forced the kernel to nest a fault handler inside IPC — the single most complex code path in the kernel. seL4 removed it entirely. Now IPC is:

• up to ~4 words in registers (zero copy, fastest path)
• up to 120 words in a per-thread IPC buffer that the kernel has already pinned — guaranteed no fault
• anything bigger: share a page and pass a capability to it

What makes it good: the kernel's worst-case IPC time is a compile-time constant. Bulk data moves by changing who can see a page, not by copying.

3. Long operations get preemption points, not blocking

Some kernel work is unavoidably long: zeroing a 1 GiB region, revoking a capability that has thousands of children. You can't block, but you also can't hold interrupts off for milliseconds.

seL4's answer: the operation is written so its progress lives in the object being modified, and the kernel periodically checks for pending interrupts. If one is pending, it returns to user space with "restart this syscall". The user thread re-issues it, and it resumes from the recorded position.

// shape of seL4's revoke loop
fn cnode_revoke(cte: &mut Cte) -> SyscallResult {
  while let Some(child) = cte.first_child() {
    delete(child);                   // progress persists in the CDT itself
    if irq_pending() {
      return SyscallResult::Restart; // unwind to empty stack, come back later
    }
  }
  SyscallResult::Done
}

What makes it good: interrupt latency is bounded and the kernel stack is empty at every preemption point. The API-visible cost is that user code must tolerate a syscall returning "not done yet" — which is exactly what a kernel with one stack has to ask.

4. Fuse the common send+wait pairs into one syscall

In an event kernel every syscall is a full trap → handle → return cycle. A client that does send(request) then recv(reply) pays two traps and, worse, between them the server might run before the client is queued as a receiver — a race the kernel has to handle.

L4's Call and ReplyRecv solve both. The client's Call atomically sends and enters BlockedOnReply. The server's ReplyRecv atomically replies to the previous client and waits for the next one. A full RPC round trip is two traps total, and the server thread is never runnable-but-idle.

client                    kernel                    server
  |                         |                         |
  |── Call(ep, msg) ───────>|  (switch directly) ────>| running handler
  |   BlockedOnReply        |                         |
  |                         |<──── ReplyRecv(ep) ─────|
  |<── reply, runnable ─────|                       server now BlockedOnReceive

What makes it good: it also enables direct process switch — the kernel hands the CPU straight from client to server without touching the scheduler's run queue, because the fused syscall tells the kernel exactly who should run next.

5. Identify the sender without a second round trip

A server handling many clients needs to know who called. Asking "who are you?" costs a syscall, and trusting a field in the message is a security hole.

seL4 badges: a capability to an endpoint can be minted with an immutable integer badge. When a message arrives through that capability, the kernel delivers the badge alongside it. The server hands each client a differently-badged cap to the same endpoint.

What makes it good: identity is authenticated by the kernel for free, and the server's dispatch is match badge { ... } — the whole event loop is one ReplyRecv in a loop with a switch.

6. Separate "signal" from "message"

Interrupts and other asynchronous events don't need a payload and must never block the signaler (a device can't wait for a driver).

seL4 Notifications are a word-sized bitmask. Signal ORs bits in and never blocks. Wait returns the accumulated mask and clears it. Multiple signals coalesce. Interrupts are delivered as notification signals, so a driver's inner loop is just Wait(notification) — identical to handling any other async event.

What makes it good: it's the "async" half of the API, it can't fail, can't block, and can't queue unboundedly (bits coalesce). Contrast Mach ports, which buffer full messages for async sends and therefore needed queue limits, back-pressure, and blocking senders — all things an event kernel can't afford.

7. Make the reply continuation an object too (MCS seL4)

Classic L4 stored "who to reply to" as a hidden per-thread reply capability in the TCB — implicit state, awkward for servers that want to defer replies or hand them to another thread.

seL4 MCS made it explicit: Reply objects. A server can receive a call, stash the reply object, go handle other clients, and reply later — or pass the reply cap to a helper thread. A SchedulingContext (a time budget) travels with the call so the server runs on the client's time, which prevents a server from being starved or used to steal CPU.

What makes it good: nothing about an in-flight RPC lives anywhere except in kernel objects the user holds capabilities to. Deferred replies, forwarding, and priority inheritance all fall out without new kernel code paths.

8. Push policy and long work out of the kernel

Because the kernel can't have long paths, anything long — page-table walks for mapping, driver logic, filesystem operations — must be a sequence of short kernel calls driven by user space.

seL4's memory API is the extreme version: there is no mmap. User space allocates page tables from Untyped memory (Retype), maps each page with an explicit Page_Map call, and handles page faults as IPC messages delivered to a handler thread. The kernel has no allocator and no paging policy at all.

What makes it good: every kernel call touches O(1) objects. The price is a verbose API, which is why real systems put a library layer on top (seL4's CAmkES, or Rust sel4-sys wrappers).

The pattern

Consideration	Good example	Anti-pattern
Waits are objects	seL4 Endpoint/Notification	Blocking read() inside a driver
Bounded, pinned payloads	L4 register IPC + pinned IPC buffer	L4 long IPC (removed)
Restartable long ops	seL4 preemption points → Restart	Holding IRQs off during revoke
Fused syscalls	Call / ReplyRecv	Separate send + recv
Kernel-authenticated identity	Badged capabilities	Sender ID in message body
Signal ≠ message	Notification bitmask	Mach async ports with queues
Explicit continuations	MCS Reply objects	Hidden reply cap in TCB
Policy in user space	Untyped + Page_Map	In-kernel allocator / mmap

If you want a Rust mental model: a good event-kernel API is one where the entire kernel could be written as fn handle(event: Event, objects: &mut Objects) -> NextThread with no await, no recursion into user memory, and every function bounded by a constant — and every API decision above is just what you have to expose to users to make that signature possible.