The SMP model

Resolves arch-interface.md finding F4 (cooperative-switch args) and generalizes per-core state, affinity, and the cross-core lock across the SMP proofs. The legacy ancestor _legacy/docs/smp-design.md (giant-lock model, Phases 0-2) stays in _legacy/ — superseded by this document and by ADR 0002.

Method. Read _legacy/docs/smp-design.md and the SMP glue in kernel/tk_kernel.c (g_sched_lock, g_sched_entering[], tk_thread_affine_here, tk_kernel_start_this_core, arch_sched_switch vs arch_context_switch), cross-referenced with the SMP proofs behind the ports in arch/: RISC-V qemu SMP (tree, risc_v), AURIX TC275 3-core (CSA-heavy, tricore — declared but not yet grafted, see arch-interface.md §7), RP2040 2-core (SIO-light, arm_v6m), plus the approach-2 sketches.

The one tension to settle first: shared pool vs per-core lists

The evidence splits two ways:

  • Tree (option A — “giant lock”): one shared TCB pool + ready selection, one scheduler spinlock, per-core current/idle/quantum. Affinity is optional (a per-TCB mask, default any-core), so threads may migrate. Proven on RISC-V qemu SMP.

  • Approach-2 sketches (option B-lite): each core owns its own ready list, threads pinned to a home core (mandatory affinity), one lock for creation. No migration. Proven on RP2040 + AURIX kernel_port. AURIX forces this because a TriCore thread’s CSA context must come from the pool of the core that runs it.

Resolution — adopt A (giant lock) + first-class affinity; it subsumes B-lite. Pinning is just “every thread’s affinity = one core.” Under the giant lock, tk_kernel_next_ready_thread already picks the most-urgent READY thread with tk_thread_affine_here(k, i); if every thread is pinned, each core only ever selects its own threads — behaviorally identical to per-core lists, via a shared pool + an affinity filter. So one model covers both: unpinned → migration (A); all-pinned → the sketches’ partitioned behavior (B-lite). Cost is the O(N) pick scan instead of an O(1) per-core list — fine for the small static TCB pool. This is the cleanest generalization, and it is exactly what kernel/tk_kernel.c does today.

The settled SMP model (verified against kernel/tk_kernel.c)

  • Giant lock: one struct tk_kernel s_kernel (accessed through the singleton pointer active_kernel), one g_sched_lock. Shared: TCB pool, ready selection, sched policy, wait queues. The lock makes select → mark RUNNING atomic across cores; the selector only considers READY, so two cores never pick the same thread.

  • What is per-core (arrays sized ARCH_CORE_COUNT, = 1 on uniprocessor so single-core is byte-identical): current_thread[], idle_index[] (one idle thread per core), g_quantum_remaining[], and the re-entry guard g_sched_entering[] — all confirmed present in tk_kernel.c / tk_kernel_internal.h.

  • The kernel lock = IRQ-off THEN spinlock (order matters — lock-then-IRQ risks taking an interrupt while holding the spinlock → deadlock):

    arch_irq_state_t s = arch_irq_save();   /* keep an ISR on THIS core out   */
arch_spin_lock(&g_sched_lock);          /* keep OTHER cores out           */
... scheduler critical section ...
arch_spin_unlock(&g_sched_lock);
arch_irq_restore(s);

    This is tk_sched_enter() / tk_sched_exit() verbatim in tk_kernel.c. On uniprocessor the spinlock is a no-op (arch_defaults.h), so this collapses to plain arch_irq_save/restore — the single-core path pays nothing.

F4 — the cooperative-switch reconcile

Three switch shapes existed across the evidence; the tree keeps two and dropped one:

Path

Mechanism

Lock convention

single-core cooperative

arch_context_switch(from, to) (explicit args)

hold-across-switch is harmless (spinlock is a no-op)

SMP cooperative

arch_sched_switch() — bare trap → tk_kernel_switch_select

lock released inside the trap, before resume

preempt (both)

tk_kernel_tick_preempt / tk_kernel_preempt_select

lock held only inside *_select

~~sketch~~

~~sched_tick + inline PendSV over g_current/g_next globals~~

superseded — a preempt-only shortcut

The invariant (the hard-won part, still enforced verbatim in tk_kernel.c): the scheduler spinlock is held only inside the *_select functions — NEVER across a context switch, an mret/rfe, or a thread’s run. Why it must be so:

  • A freshly created thread enters straight at its function and never reaches an unlock — if the lock were held across the switch, the other core deadlocks. Holding it only inside *_select means a new thread starts with the lock already free → no entry trampoline needed.

  • tk_kernel_wait() keeps the lock from enqueue → mark BLOCKED → save-in-trap on the SMP path (arch_sched_switch(), called with the lock held), which closes the lost-wakeup race (another core can’t ready+run the thread before it’s saved). On single-core the lock is dropped before the yield — there is no other core to race.

So F4 is resolved: the sketches’ g_current/g_next globals were the single-core “hold-across” convention in disguise; the general model uses explicit from/to for single-core cooperative and select-in-trap for SMP, both gated on ARCH_CORE_COUNT > 1 (#if ARCH_CORE_COUNT > 1 in tk_kernel.c and tk_kernel_port.h), single-core byte-for-byte unchanged.

Two hard-won SMP details to carry forward (do not re-derive)

  • The tk_kernel_start_this_core deadlock + the re-entry guard. A core enters its per-core start holding g_sched_lock with interrupts on (it’s about to launch its first thread); a tick/IPI landing there would re-enter preempt_select and self-deadlock on the held lock. Fixed with a per-core flag g_sched_entering[cpu] that tk_kernel_preempt_select checks and bails on — not by masking IRQs (masking only moved when the tick landed and inverted a real 2-core/3-core failure). HW-proven on AURIX 3-core; the guard array and both check sites are live in tk_kernel.c today (tk_kernel_tick_preempt, tk_kernel_preempt_select, tk_kernel_start_this_core).

  • The spinlock is TTAS-shaped, fairness deferred. A fair ticket lock (cmpswap.w fetch-add) was sketch-sound and clean on AURIX smp5/smp7 but wedged smp6 on hardware (cause not root-caused). Shipped = test-and-test-and-set — risc_v’s arch_spin_lock (arch/risc_v/kernel_arch.h) is a literal TTAS (__sync_lock_test_and_set then spin read-only); RP2040’s software lock word is made atomic by a SIO hardware meta-spinlock in the same acquire/retry shape (boards/rp2040_pico/tk_smp_rp2040.c). Starvation is bounded at the source by arch_idle() dwelling. Revisit fairness only after reproducing the smp6 wedge under a debugger.

Affinity (proven — keep as first-class, config-gated)

Per-TCB affinity bitmask, default 0xFFu (any core) — set in tk_thread_create_core. tk_thread_affine_here(k,i) = (affinity >> arch_core_id()) & 1; tk_thread_set_affinity(t, mask) / tk_thread_pin(t, core). Off → the pick loop is identical to uniprocessor. This is the single field that makes the giant lock subsume the pinned model (above). At root this is TK_FEAT_AFFINITY, compiled in only when TK_CONFIG_ENABLE_AFFINITY is set and ARCH_CORE_COUNT > 1 (kernel/tk_config.h) — on a single-core build the field and the check both compile out.

  • ARCH_HAS_LAZY_CONTEXT implies mandatory single-core affinity. On register- window / CSA archs (TriCore) a thread’s context must be materialized from the pool of the core that runs it, so the thread cannot migrate. Such a port pins each thread to its home core and materializes on first dispatch (arch_context_prepare, gated by the capability flag — see tk_kernel_preempt_select’s #if defined(ARCH_HAS_LAZY_CONTEXT) block). This coupling is explicit: lazy-context ⇒ affinity is forced, not optional.

Round-robin fairness across cores (phase-offset first slice)

The per-core round-robin (tk_kernel_next_ready_thread scans from THIS core’s current

    1. is provably fair — verified by a host simulation of the exact selection logic: equal work per thread at every tick phase, on equal-speed cores. There is exactly one degenerate case: when the cores’ quantum expiries land on the same tick (their per-core SysTicks in phase), both cores switch together and the round-robin settles into a stable per-core partition — threads stop migrating, each pinned to its initial core. That is fine on a HOMOGENEOUS SMP (fair, and cache-local), but on HETEROGENEOUS cores — e.g. a core that boots Non-secure and runs measurably slower — it pins some threads to the slow core and skews their work share (HW-observed ~27% on the bring-up board that surfaced this).

Fix (HW-verified, live in tk_kernel_start_this_core): phase-offset each core’s FIRST slice so expiries interleave rather than coincide — core c starts at q·(1 − c/N) (core0 = full quantum, core1 = half, …). The switch points de-sync, every thread cycles across all cores, and work is fair even when the cores differ in speed (skew 27% → <0.5% measured). Negligible cost on Cortex-M (no L1 D-cache). Single-core (cpu==0) is unchanged. It is a one-time phase establishment; a dynamically re-phasing workload (a periodically-migrating thread) can transiently re-partition, but the cumulative distribution stays even. The heterogeneous core-speed difference itself is a HW property (a security-state execution penalty), not a fairness bug; the EXC_RETURN security reconciliation in arch/arm_v8m is what makes such a split safe at all.

The arch Tier-2 contract (from arch-interface.md)

ARCH_CORE_COUNT, arch_core_id, arch_spinlock_t + arch_spin_{init,lock,unlock}, arch_ipi, arch_smp_start, arch_sched_switch. The atomic primitive behind the spinlock is the only per-arch variance, and the proofs span the range:

Arch

core id

spinlock atomic

IPI

secondary start

RISC-V (risc_v)

mhartid

AMO amoswap.w (__sync) + fence

CLINT MSIP

park-in-startup, release

AURIX (tricore, unimplemented at root)

CORE_ID CSFR

swap.w/cmpswap.w (__sync)

GPSR service req

IfxCpu_startCore / SDK

RP2040 (arm_v6m)

SIO CPUID

SIO hardware spinlock (M0+ has no LDREX)

SIO FIFO

multicore_launch_core1

All fit the same Tier-2 surface; single-core inherits the no-op defaults from arch/arch_defaults.h. The AURIX-heavy vs RP2040-light gap reduces to exactly one bit: ARCH_HAS_LAZY_CONTEXT (CSA materialization) — everything else is the same contract with a different atomic.

Separate-kernel AMP: in scope (ADR 0002)

The approach-2 experiments referenced here were labelled “SMP+AMP,” but what they actually built was never separate kernels: one SMP kernel scheduling both cores (per-core ticks, both preempt-scheduling), plus an application-level cross-core handoff — a producer thread on one core handing jobs to a consumer on another over an inter-core FIFO. That is SMP with pinned threads and a cross-core message primitive, not a second scheduling model, and it is still a reasonable way to describe a lightweight cross-core mailbox layered on arch_ipi (an IPC concern, not a scheduler concern).

Separate-kernel AMP — multiple independent struct tk_kernel instances, each owning a disjoint subset of cores — was an open question when this document was first written. It is no longer out of scope: it was HW-proven twice (RP2040 two-instance 1+1, and AURIX TC275 “2 SMP + 1 aside” — one instance owning a real 2-core SMP domain beside a disjoint 1-core AMP island), and ADR 0002 generalizes the singleton above into per-instance kernels resolved per physical core — the same scheduler model, replicated N times, not a new one. Every mechanic this document settles (the giant lock, per-core current/idle/quantum/entering, select-in-trap with the lock held only inside *_select, the g_sched_entering re-entry guard, phase-offset first slice, TTAS-not-ticket lock, ARCH_HAS_LAZY_CONTEXT ⇒ mandatory affinity) is preserved per instance; ADR 0002 only lifts the singleton / single-scheduling-domain scope limit. The graft into kernel/tk_kernel.c is tracked there, not here — this document describes the mechanics one instance uses, which do not change.

What this settles

  • Settled: giant-lock + first-class affinity (subsumes the sketches’ per-core pinned model); per-core current/idle/quantum/entering; the kernel-lock pair (IRQ-off then spinlock, no-op single-core); F4 — explicit from/to single-core vs select-in-trap SMP, lock held only inside *_select; the g_sched_entering re-entry guard and TTAS-not-ticket lock (both HW-hardened); affinity forced under ARCH_HAS_LAZY_CONTEXT.

  • The whole AURIX↔RP2040 SMP delta = ARCH_HAS_LAZY_CONTEXT plus the spinlock’s atomic; the rest of the model is identical.

  • Separate-kernel AMP is in scope via ADR 0002 — see that document for the un-globaling plan and current status.

  • See also: arch-interface.md (the Tier-2 contract this model consumes) and tick-policy.md (how the tick feeds tk_kernel_tick, shared by every core).