danos/docs/smp.md

# SMP: multiple cores, the microkernel way

A design/research note, not built yet. danos runs on **one core** today (see
[scheduling.md](scheduling.md)); this maps how microkernels — especially the L4
family and seL4 — handle **symmetric multiprocessing (SMP)**, so the eventual port
has a plan and a reading list. It also flags where those choices depend on whether
danos is chasing **real-time** or **resilience** (see the note at the end).

## First, the vocabulary

Three independent things people conflate (see [scheduling.md](scheduling.md) for the
danos specifics):

- **Task capacity** (`max_tasks`) — how many tasks can *exist*. A table size.
- **Cores** — how many tasks *run at the same instant*. One running task per core.
- **Real-time** — whether timing is *predictable*. Comes from bounded operations
  (our O(1) scheduler), not from core count.

danos is uniprocessor today: one global `current` task, one set of ready queues, one
timer. Even on an 8-core CPU, the firmware starts only the **bootstrap processor
(BSP)**; the other cores (**application processors**, APs) sit parked until the
kernel wakes them, which it doesn't yet.

## The common microkernel instinct: don't share kernel state

Monolithic kernels (Linux) share large amounts of state across cores behind many
fine-grained locks. Microkernels lean the other way — the kernel does *little* (IPC,
scheduling, capabilities), so the pressure is to make kernel state **per-core** and
coordinate cores with **inter-processor interrupts (IPIs) or messages** rather than
shared, locked data structures. Two hallmarks follow:

- **Thread-to-core affinity.** Threads are usually *bound* to a core; migration is an
  explicit operation, not automatic load-balancing.
- **Policy in user space.** *Which* core a thread runs on tends to be a user-level
  decision (a scheduler/manager server); the kernel just provides the mechanism to
  run it there and to signal across cores. This matches the microkernel creed:
  mechanism in the kernel, policy outside.

Within that instinct, the L4 family split on **how much to lock**.

## seL4: the "big kernel lock" — and why it's not a hack

seL4's choice is striking: a **single big kernel lock (BKL)**. Only one core runs
*kernel* code at a time; **user code runs fully in parallel** on all cores. A core
that traps into the kernel takes the global lock, does its (short) work, releases it.

Why so coarse? **Formal verification.** seL4's whole value is a machine-checked
correctness proof, built for a *uniprocessor* kernel — reasoning about one thread of
kernel execution. Fine-grained SMP locking explodes the interleavings you'd have to
reason about. The big lock **serialises kernel execution so the single-core reasoning
still holds**. It trades kernel scalability for verifiability.

And it works better than it sounds, *because the kernel does so little*: the lock is
held for short, bounded intervals, while the real work (drivers, services) runs in
user space in parallel, outside the lock. Scheduling is otherwise **per-core** (each
core its own ready queues), threads carry an **affinity**, and cross-core IPC costs an
IPI.

> Nuance: the fully *verified* seL4 configuration is the uniprocessor one. The
> SMP/big-lock version isn't covered by the same end-to-end proof — extending
> verification to multicore has been ongoing research. So the big lock is partly
> "stay close to the thing we proved."

seL4 also layers **MCS** (mixed-criticality scheduling) on top: **scheduling
contexts** carrying a time *budget* and *period*, so a thread can't overrun its share
— temporal isolation, reasoned about per core. This is the seriously real-time part.

## Fiasco.OC / NOVA: per-CPU, finer-grained

Not all L4s took the big lock. **Fiasco.OC** (TU Dresden L4, part of L4Re) is
**per-CPU**: per-CPU run queues, CPU-local kernel objects, IPIs for the rare
cross-CPU operations. Threads bind to a CPU; moving one is explicit. Scales better
than a big lock, more complex, and without seL4's verification constraint forcing the
issue. **NOVA** (a microhypervisor) is similarly per-CPU. The shared pattern: make
everything CPU-local you can, and when cores must interact, **send a message/IPI**
instead of touching shared data.

## The extreme: the "multikernel"

Taken to its logical end you get **Barrelfish** (ETH Zurich): treat a multicore
machine as a *network of cores*, each running its **own kernel instance**, sharing
**no** kernel memory, communicating **only by message passing** — the microkernel's
IPC philosophy applied to the kernel's own structure. seL4's "clustered multikernel"
explorations use the same idea: groups of cores, each cluster a big-lock domain,
clusters talking by messages. The insight: if you're already committed to messages
for user-space isolation, structure the kernel across cores the same way and sidestep
shared-memory locking entirely.

## Does the right choice depend on real-time vs resilience?

Yes — and this is the branch that matters for danos right now.

- **If the goal is hard real-time:** favour **per-core scheduling with fixed
  affinity**. A thread never gets surprise-migrated mid-deadline, and each core's
  timeline can be reasoned about in isolation. Global load-balancing (Linux's default)
  is great for throughput and *bad* for determinism, which is why RT microkernels
  mostly pin threads. seL4's MCS scheduling contexts are the reference model.
- **If the goal is resilience / restartability:** the SMP priority shifts to **fault
  isolation and recovery**, not timing. What matters is that a failed component (a
  driver, a service) on any core can be **killed and restarted** without taking the
  system down — which is a property of address-space isolation + a supervising
  restart server (below), *largely orthogonal to how cores are scheduled*. A big lock
  is perfectly fine here; you're optimising for "a crash is contained and
  recoverable," not "latency is bounded to N µs."
- **If the goal is throughput:** you'd care about lock contention and per-core
  queues — the least microkernel-flavoured of the three.

These pull in different directions, so **picking the primary goal comes before
picking the SMP design.** (danos's founding assumption was real-time; that's under
active reconsideration in favour of resilience — see [vision.md](vision.md).)

## What this would mean for danos

Whatever the top goal, the *sequence* is the same and seL4 validates starting simple:

1. **Enumerate cores** — needs [device discovery](discovery.md) (ACPI MADT on x86,
   device tree on ARM). SMP is a concrete consumer of that work. **Done on x86:** the
   MADT parse records every usable Local APIC — with the `apic_id` an AP wake targets —
   and `platform.cpus()` returns the list (see [discovery.md](discovery.md)). The boot
   log reports the count; the ARM (device-tree) path still needs it.
2. **Wake the APs** — INIT–SIPI–SIPI on x86; PSCI/spin-tables on ARM. Each core brings
   up its own tables, timer, and idle task.
3. **Start with a big kernel lock.** It's a legitimate first design, not a shortcut —
   philosophically aligned with a tiny kernel, and it lets the single-core correctness
   model you already have (the interrupt-flag discipline in
   [scheduling.md](scheduling.md)) stay largely intact: one lock around kernel entry
   instead of rethinking every critical section.
4. **Later, if contention bites,** evolve toward **per-core run queues + explicit
   affinity** (the Fiasco.OC direction) — also the more real-time-predictable model.
5. **Placement stays a user-space policy** — the kernel runs a thread on the core it's
   told to, a user-level manager decides which.

Big-lock-first → per-core-later. The affinity/MCS depth is only worth it if real-time
turns out to be the actual goal.

## Further reading

**Microkernel SMP & scheduling**
- Klein et al., *"seL4: Formal Verification of an OS Kernel"* (SOSP 2009) — the
  verification that shapes seL4's whole SMP stance.
- Lyons et al., *"Scheduling-Context Capabilities: A Principled, Light-Weight OS
  Mechanism for Managing Time"* (EuroSys 2018) — seL4 MCS, the real-time model.
- The **seL4 whitepaper** and "towards a verified multiprocessor seL4" material — the
  big-lock / clustered-multikernel reasoning.
- **Fiasco.OC / L4Re** documentation (TU Dresden) — the per-CPU alternative.
- Baumann et al., *"The Multikernel: A New OS Architecture for Scalable Multicore
  Systems"* (SOSP 2009) — Barrelfish, the share-nothing extreme.

**Resilience / self-healing (if that's the real goal)**
- Herder et al., *"Fault Isolation for Device Drivers"* and the **MINIX 3**
  *reincarnation server* — a driver crashes, a supervisor restarts it live. The
  closest existing system to "re-initialise parts of the OS."
- **QNX** — commercial microkernel RTOS built on message passing and restartable
  drivers; good study of the combination.
- **Erlang/OTP** *supervision trees* and the *"let it crash"* philosophy — not a
  kernel, but the canonical design for "isolate failures and restart the failed
  part," directly relevant to danos's restartability motivation.

## Related

- [scheduling.md](scheduling.md) — the single-core scheduler SMP would extend.
- [discovery.md](discovery.md) — enumerating cores is a device-discovery problem.
- [ipc.md](ipc.md) — the message passing cross-core coordination rides on.
- [vision.md](vision.md) — the goals question (real-time vs resilience) this note
  keeps bumping into.