Skip to content

docs(gust): two-level partition scheduler + tiered supervision design — FOR REVIEW, do not merge (gale#63)#175

Open
avrabe wants to merge 1 commit into
mainfrom
design/gust-partition-scheduler
Open

docs(gust): two-level partition scheduler + tiered supervision design — FOR REVIEW, do not merge (gale#63)#175
avrabe wants to merge 1 commit into
mainfrom
design/gust-partition-scheduler

Conversation

@avrabe

@avrabe avrabe commented Jul 11, 2026

Copy link
Copy Markdown
Contributor

Design doc for review — not for merge yet (brainstorming-gated; awaiting your approval before an implementation plan).

Captures the partition-scheduler design validated with jess on gale#63:

  • Two-level model: 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.
  • 3-core RT1176 map: M7 flight-control / M4 estimation / F100 = cross-core Health Monitor (two-tier HM: per-core 653 window-end preemption + physically-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 (from the verified-scheduling survey): DWT = high-water-mark not certification-grade WCET; migration below the safety line; reject Vestal-style dropping; verified ≠ timing-verified.
  • gale-side critical path: the async executor (epic Add Renode emulation tests for Cortex-M4F and Cortex-M33 #3), Embassy-class, Verus: no-lost-wakeups / bounded-poll / fair-ready-queue. v1 = static single-partition slice (buildable now); v2 rides meld#326.

Doc: docs/superpowers/specs/2026-07-11-gust-partition-scheduler-design.md. Please review; on approval I'll turn it into an implementation plan (executor + Verus harness first).

🤖 Generated with Claude Code

… (gale#63)

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) <noreply@anthropic.com>
@codecov

codecov Bot commented Jul 11, 2026

Copy link
Copy Markdown

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant