9.3 KiB

Raw Blame History

SMP: multiple cores, the microkernel way

A design/research note, not built yet. danos runs on one core today (see 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 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.

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

What this would mean for danos

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

Enumerate cores — needs device discovery (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). The boot log reports the count; the ARM (device-tree) path still needs it.
Wake the APs — INIT–SIPI–SIPI on x86; PSCI/spin-tables on ARM. Each core brings up its own tables, timer, and idle task.
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) stay largely intact: one lock around kernel entry instead of rethinking every critical section.
Later, if contention bites, evolve toward per-core run queues + explicit affinity (the Fiasco.OC direction) — also the more real-time-predictable model.
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.

9.3 KiB Raw Blame History Unescape Escape