# 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 mid-transition. The firmware starts only the **bootstrap processor (BSP)**;
the other cores (**application processors**, APs) sit parked until the kernel wakes
them. As of the SMP work in progress (see [Implementation status](#implementation-status)
below), danos now *does* wake the APs — each climbs to 64-bit long mode and reports
in — and the shared kernel state (scheduler queues, IPC) is already serialised behind
a big kernel lock. What's not done yet is letting the woken APs actually run tasks;
`current` is per-CPU but the run loop is still BSP-only.

## 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. **In progress on x86** — the cores reach
   long mode and park; the per-core tables/timer/scheduler entry is the next step
   ([status](#implementation-status)).
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. **Done** — see
   `src/kernel/sync.zig`.
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.

## Implementation status

The "wake + schedule" build (real parallel task execution) is going in as a sequence
of green checkpoints — each step keeps the single-core test suite passing before the
next lands.

**Done:**

- **Core enumeration** — the MADT parse records every usable Local APIC (with its
  `apic_id`, which an AP wake targets); `platform.cpus()` returns the list. See
  [discovery.md](discovery.md).
- **The big kernel lock** (`src/kernel/sync.zig`) — one coarse spinlock guarding the
  scheduler queues and IPC, always held with local interrupts disabled. It is held
  *across* a context switch and released by whichever task resumes (the hand-off
  rule); `task_trampoline` releases it for a freshly-spawned task. `scheduler.zig` and
  `ipc.zig` run every critical section under it. Uncontended on one core, so behaviour
  is identical to the old interrupt-flag model.
- **Per-CPU state** — a `PerCpu` struct (running task, idle task, APIC id) per core,
  its pointer kept in the x86 **GS base** (`IA32_GS_BASE`; no `swapgs`, since there's
  no user mode yet). The old global `current` is now `thisCpu().current`. The ready
  queues stay **global** under the lock — work-conserving, so any idle core will pull
  the highest-priority ready task; per-core queues are a later optimisation.
- **AP wake to long mode** — `arch.startSecondary` drives INIT–SIPI–SIPI (via the
  LAPIC ICR) to wake each parked core one at a time. A woken core starts in 16-bit
  real mode at a low page and runs the [trampoline](../src/kernel/arch/x86_64/trampoline.s)
  up through protected mode into 64-bit long mode, then lands in `smp.zig:apEntry`,
  publishes its per-CPU pointer, and reports in. Verified in QEMU with `-smp 4`:
  all four cores report `online`.

  The trampoline earns its complexity from three hardware facts:
  - a STARTUP IPI vectors a core to physical `vector << 12` (a *byte* vector), so the
    trampoline must live **below 1 MiB** — the kernel reserves that page from the frame
    allocator at boot, before paging/heap draw down the scarce low frames;
  - the blanket RAM identity map is **NX** (W^X), but the AP fetches the trampoline
    from it under paging, so that one page is made executable for bring-up;
  - the blob is copied to a page whose address isn't known at link time, so it is
    **position-independent**: it derives its own base from `CS` and, crucially,
    addresses data *segment-relative in real mode* (where the segment base already
    supplies the page base) but *base-register-relative in protected/long mode* (flat
    segments, base 0). Getting that distinction wrong was the first bug found.

**Next:**

- **Per-core descriptor tables + scheduler entry** — each AP needs its own TSS (its
  own IST/`rsp0` stack) and to load the kernel GDT/IDT, enable its LAPIC timer, and
  enter the scheduler run loop under the big lock. (The 3a checkpoint deliberately
  parks the APs on the trampoline's tables with interrupts off; loading the shared
  kernel GDT on an AP faulted, and the per-core-TSS work is where that's resolved.)
- **A parallelism test** — a case where N cores drive N counters at once, proving work
  runs truly in parallel rather than just that the APs booted.
- **IPIs** (deferred) — cross-core wake/preempt. Not needed for correctness: an idle
  core wakes on its own timer tick and pulls ready work then; IPIs only cut that
  latency from ≤1 ms to near-instant.

## 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.