documenting smp and scheduling to research

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

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.

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 stack_size = 16 * 1024; // each task's kernel stack is 16 KiB
-const max_tasks = 16;
+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 };