From a660993925c36585fe805ecca1c31b31d1cff14b Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sat, 11 Jul 2026 12:11:39 +0200 Subject: [PATCH] docs(gust): two-level partition scheduler + tiered supervision design (gale#63) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Validated with jess on gale#63: outer ARINC 653 fixed-priority time-partitioned preemptive backbone + inner cooperative kiln-async inside a bounded partition window; safety lives in the outer timer + Health Monitor, not inner good behaviour (non-maskable window-end preemption contains a hogging task by construction). 3-core RT1176 map: M7 flight / M4 estimation / F100 = cross-core HM. Two-tier HM (per-core 653 window-end + independent F100 backstop + wdg-thin IWDG module backstop). Small verified switch/HM core (seL4-MCS scheduling-context shape); synth stays out of the flight TCB. Honesty constraints baked in (from the verified-scheduling research survey): DWT is measurement-based high-water-mark NOT certification-grade WCET; migration stays below the safety line (static F100 redundancy, not dynamic); reject Vestal-style mixed-criticality dropping; verified ≠ timing-verified. gale-side critical path = the async executor (epic #3), Embassy-class, Verus: no-lost-wakeups / bounded-poll / fair-ready-queue. v1 = static single-partition slice (unblocked NOW); v2 rides meld#326 reloc-consumer (gale-side reloc cores already solved, gale#168). Co-Authored-By: Claude Opus 4.8 (1M context) --- ...6-07-11-gust-partition-scheduler-design.md | 166 ++++++++++++++++++ 1 file changed, 166 insertions(+) create mode 100644 docs/superpowers/specs/2026-07-11-gust-partition-scheduler-design.md diff --git a/docs/superpowers/specs/2026-07-11-gust-partition-scheduler-design.md b/docs/superpowers/specs/2026-07-11-gust-partition-scheduler-design.md new file mode 100644 index 0000000..b77f24f --- /dev/null +++ b/docs/superpowers/specs/2026-07-11-gust-partition-scheduler-design.md @@ -0,0 +1,166 @@ +# gust two-level partition scheduler + tiered supervision — design + +**Status:** design (validated with jess on gale#63; awaiting user review before an +implementation plan). +**Date:** 2026-07-11. +**Origin:** user ask ("kiln async should do more — priority tasks + supervision"), the +ASIL-D / actually-lands reframe, a verified-scheduling research survey, and jess's +gale#63 endorsement + 3-core RT1176 mapping. + +## 1. Problem & goal + +gust's async today is `gust:os/spawn` — cooperative, scalar, dissolved-to-native +(`gust_poll` = kiln `poll_round`). Cooperative-only gives no bounded latency and no +freedom-from-interference when a task faults or over-runs. For a flight target you land +(Pixhawk 6X-RT / i.MX RT1176), the scheduling **backbone** must be certifiable. Goal: +add priority scheduling + fault supervision **without inventing a novel scheduler** — +keep the proven backbone, make what's new be its *size*, its *verification*, and the +ergonomics that ride on top. + +## 2. The two-level model (endorsed by jess, research-confirmed canonical IMA) + +- **Outer — fixed-priority, time-partitioned, preemptive** (ARINC 653 major-frame / + AUTOSAR-OS timing-protection). A trusted timer-tick does a partition switch; each + partition gets a guaranteed, offline-planned time window; temporal + spatial isolation + enforced. This is the certifiable "no other way" backbone. +- **Inner — cooperative kiln-async inside a partition's window.** The dissolved async + tasks (`poll_round`) run within one partition's window — where the "superior + experience" (zero-alloc, dissolved, capability-isolated ergonomic async) lives, made + safe by being boxed in a preemptive partition. + +**The load-bearing safety property (jess underlined it):** safety lives in the **outer +timer + Health Monitor, not in inner good behaviour.** A non-yielding cooperative task +is contained *by construction* by the **non-maskable window-end preemption** — which +therefore MUST live in the verified core and be un-maskable by inner code. The survey +confirmed "cooperative scheduling inside a bounded preemptive window" is an explicitly +accepted composable-scheduling pattern; the assessor's burden is *bounding the window*, +not the inner discipline. + +## 3. 3-core RT1176 partition mapping (jess owns the OS/silicon side) + +| core | outer partition (ARINC 653) | inner (kiln-async) | role | +|---|---|---|---| +| **M7** (fpv5-d16) | flight-control window (~1 kHz) | falcon cascade, one fused async component | flight partition | +| **M4** (fpv4-sp) | estimator window | IEKF, one fused async component | estimation partition | +| **F100** (M3, 8 KB) | — | gust failsafe (fixed-point, DD-011) | **cross-core Health Monitor** | + +Each partition hosts exactly one fused async component (jess's epic model: one fused +component per thread/partition, multiple across cores). + +## 4. Two-tier Health Monitor (the "both, tiered" supervision) + +The tiered supervision the user chose maps onto the ARINC 653 Health Monitor, and jess's +mapping makes it **two physical tiers**: + +1. **Per-core (tier 1):** the 653 window-end preemption on M7/M4 + AUTOSAR-style budget + monitoring. Within a partition: process-level restart of a faulting inner task + (availability), bounded by a restart-count + cooldown, escalating to partition + fail-to-safe on repeated fault / budget-overrun / deadline-miss. +2. **Cross-core (tier 2):** the **physically independent F100** running gust is the + ultimate spatial+temporal containment for the two FMU cores. It already consumes the + M7↔M4 MU heartbeat (gale#65 doorbell datapath, proven in the 3-core Renode model) and + trips the 4× failsafe-PWM on FMU loss / window overrun. Stronger than a single-core HM + — it's the gust story we already have. +3. **Module (tier 0 backstop):** the **wdg-thin IWDG driver** (cannot-un-start, + Kani-proven) as the hardware fail-to-safe if a HM core itself hangs (loss of service → + HW reset). + +Escalation is provably terminating (bounded restart-count → partition fail-to-safe → +cross-core F100 trip); the HM policy is a small FSM verified with Kani/Verus. + +## 5. The verified TCB boundary + +- **Trusted + proven (small):** the partition-switch + HM core — seL4-MCS + *scheduling-context-capability* shape (time as a budget/capability), an mmio + scalar-FSM + sliver with no heap, matching the thin-seam driver TCB discipline. Precedent for a + *small* verified isolation core: seL4 MCS (functional correctness proven), Muen (SPARK), + ProvenCore. +- **Untrusted / dissolved (outside the core):** apps, drivers, the async machinery — all + dissolved capability-components. **synth stays out of the flight TCB.** The TCB grows + from ~0 to "a small proven scheduler," still radically smaller than a conventional + certified RTOS. + +## 6. Honesty constraints & non-goals (from the research survey) + +These are hard lines, not preferences: + +- **DWT ≠ certification-grade WCET.** DWT cycle counts (our 1.448×/1.839× silicon anchors) + are *measurement-based* → **high-water-mark**, and unsound on multicore. DO-178C/DO-333 + want a *sound* bound (static analysis). Our DWT numbers are **evidence + regression + guards**; DAL-A partition budgets need static WCET (or hybrid + provable path coverage) + + margin, stated explicitly. (Discipline: verification-claims-honesty.) +- **Migration stays strictly below the safety line.** Checkpoint/restart + task migration + (the kiln#415 interpreted-tenant rung) are availability-only / non-critical / + redundant-lane; the safety function recovers by **local fail-to-safe**, and redundancy + is *static* (the independent F100), never dynamic migration on the critical path. +- **Reject Vestal-style mixed-criticality dropping.** Deployable MC = static partition + isolation, not "drop low-crit on a mode switch." Criticalities live in separate + partitions; inner tenants share a partition only at a shared assurance level. +- **Verified ≠ timing-verified.** Prove functional correctness of the switch/HM core + mechanically; treat WCET/timing as a *separate, partly-manual* soundness case (seL4's + own gap). Do not conflate the two. +- **New hazard to log:** multicore / shared-bus temporal interference on the RT1176 + (M7 + M4, shared bus + XIP) — outside every prior proof; needs its own safety-case entry + and mitigation. (Partly answered by the independent F100 tier.) + +Locks that cross the verified core / inter-partition channels use **PCP/ICPP** (immediate +priority ceiling; DO-178B-certified, deadlock-free), with the ceiling proven ≥ max user +priority — not plain PIP. + +## 7. The gale-side critical path: the executor (epic #3) + +jess's one open dependency on our side: the inner layer needs the **async executor** — +Embassy-class, `no_std`, dissolved — with **Verus** proof obligations: + +- **no-lost-wakeups** — a set ready-bit is never dropped. +- **bounded-poll** — each `poll_round` visits each ready task at most once; terminates. +- **fair-ready-queue** — highest-priority-ready runs; work-conserving; no starvation + within a partition window. + +This is the concrete next gale deliverable that gates the whole inner layer. It composes +with epic #5 (AMP + the MU as cross-core transport) for the tier-2 HM datapath. It also +subsumes kiln#415 (the interpreter as the migratable-tenant rung — availability tier only). + +## 8. Shippable increments + +- **v1 (buildable NOW, unblocked lane):** a **static single-partition** slice — the + cooperative async executor in one fixed window + the verified HM policy FSM (bounded + restart → fail-to-safe) + the wdg-thin HW backstop. Single-component / stateless-read + dissolve → **not meld#326-gated**. Kani/Verus-prove the executor + HM FSM, dissolve + 0-/bounded-SRAM, gate on Renode. This proves the inner layer + supervision without + multi-partition preemption. +- **v2 (rides meld#326):** multi-partition preemptive time-partitioning + dynamic spawn. + The gale-side reloc-core production is already solved (gale#168, `--emit-relocs`); v2 + waits on meld's reloc-consumer to fuse the multi-provider node cleanly. +- **v3:** the full 3-core mapping in the Renode model (jess wires the 653 outer window + + kiln inner; the F100/gust HM tier is already demonstrable there). + +## 9. Traceability & toolchain fit (feature-loop step 1 = architecture in spar) + +- **spar:** jess models the ARINC 653 partitioning in `hardware/pixhawk6x-rt.aadl` — + partition windows + Health Monitor — and runs spar's ARINC 653 partitioning + + modal-scheduling analysis (adds the *temporal* layer the model was missing; the + partition→core `Actual_Processor_Binding` is already there). Inter-partition interfaces + stay spar-generated WIT (REQ-PIX-007: `wit/{falcon,estimator,failsafe}.wit`). +- **rivet:** the two-level model, the HM policy, and the DWT-vs-static-WCET honesty + boundary as typed requirements/decisions; ASIL-D/DAL decomposition. A jess DD records + the two-level model + F100-as-cross-core-HM mapping. +- **Renode:** the 3-core model (gale#65 MU doorbell) is the proving ground; the F100/gust + HM tier is already demonstrable. + +## 10. Open items + +- Exact certification target (DAL letter / ISO 26262 ASIL-D) — jess owns; sets the WCET + justification bar. +- Static-WCET toolchain choice for the DAL-A partition budgets (the DWT numbers don't + suffice). +- The executor's Verus harness (no-lost-wakeups / bounded-poll / fair-ready-queue) — the + first implementation artifact. +- Multicore/shared-bus interference mitigation on RT1176 — safety-case entry. + +## 11. Non-goals + +Not a novel scheduling algorithm; not a full RTOS; not dynamic migration on the critical +path; not a claim that DWT gives certification WCET. This design keeps the certifiable +ARINC 653 backbone and contributes the small verified core + the dissolved cooperative +inner layer.