diff --git a/docs/README.md b/docs/README.md index 6d1a413..77cde6c 100644 --- a/docs/README.md +++ b/docs/README.md @@ -57,6 +57,9 @@ Cutting across all of these: - **[discovery.md](discovery.md) — device discovery.** A design note (not built yet) on learning what hardware exists via ACPI (x86) or device tree (ARM) behind one neutral device model — when to build it, and how to keep it architecture-agnostic. +- **[smp.md](smp.md) — multiple cores.** A design/research note on how microkernels + (L4, seL4) handle SMP — big kernel lock vs per-CPU vs multikernel — and how the + right choice depends on whether danos is chasing real-time or resilience. - **[sysv.md](sysv.md) — the calling convention.** What "the kernel is SysV" means, and why the loader→kernel boundary has to pin it (the RDI-vs-RCX handoff). - **[testing.md](testing.md) — testing.** How the kernel is tested by booting it in diff --git a/docs/smp.md b/docs/smp.md new file mode 100644 index 0000000..99b4717 --- /dev/null +++ b/docs/smp.md @@ -0,0 +1,162 @@ +# 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. +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. diff --git a/src/sched.zig b/src/sched.zig index da48944..2ea3858 100644 --- a/src/sched.zig +++ b/src/sched.zig @@ -18,8 +18,8 @@ const heap = @import("heap.zig"); pub const Priority = u3; const num_priorities = 8; -const stack_size = 16 * 1024; // per-task kernel stack -const max_tasks = 16; +const stack_size = 16 * 1024; // each task's kernel stack is 16 KiB +const max_tasks = 16; // the maximum number of tasks alive at once is 16 in a static sized pool const State = enum { free, ready, running, blocked };