gale as composable OS components: a first-class 'build-your-own OS' mode (C-free Rust+wasm), beyond the Zephyr integration

[avrabe]

The reframe (from jess's RT1176 + gust work)

Working the Pixhawk 6X-RT bring-up, a nice realization fell out: gale isn't really "verified Zephyr primitives" — it's a library of composable, formally-verified OS components, usable two ways:

1. Drop into an existing OS — the zephyr/*.c integration track (gale replaces Zephyr's C kernel primitives in place). Proven: 36 QEMU suites.
2. Construct your own OS — compose gale primitives + kiln (scheduler) + an async HAL substrate + wasm driver bodies into a bespoke, purpose-built OS. gust is the first instance (bare Cortex-M3, no Zephyr).

jess wants mode (2) for the flight stack — and the payoff is that the C disappears: no Zephyr, no NuttX/PX4, no NXP SDK C drivers. The flight TCB becomes verified Rust (gale + kiln + HAL) + wasm (Kani-proven drivers + falcon) — one language discipline, one verification story end-to-end (Verus/Rocq/Lean + Kani), the smallest auditable trusted base, and the same OS at three scales: M7 (falcon) / M4 (sensor-I/O offload) / F100 (gust). (The only non-Rust residue — the i.MX boot ROM — is out of the flight path; it's touched only by the on-ground update bootloader. jess DD-016.)

The driver model (the sophisticated piece Zephyr's C otherwise gives you)

gust's driver model is trivial (a ~4-item sync native shim). The M7 needs the real thing — DMA, async completion, multiple isolated buses, redundancy. We think the clean substrate is:

• Seam anchored on embedded-hal-async (the standard async embedded-HAL traits).
• Native host substrate = Embassy-class async HAL (bus transport + DMA + IRQ-completion) — "drivers as host components, driven down."
• Executor = kiln-async (which is already Embassy-inspired — its design cites embassy-executor's task-arena/waker-as-index).
• Verifiable logic stays wasm — relay's Kani-proven protocol decode + the redundancy voting sit above the async traits.

So: verify what's verifiable (decode/voting in wasm), reuse battle-tested for the timing/DMA you can't easily prove (async HAL). This is jess DD-012/DD-015 (the relay↔jess seam) made concrete for async+DMA, the full-fat version of the gust seam.

The enabler we just found

The MIMXRT1176 CMSIS-SVD (NXP official, BSD-3-Clause, cm7 + cm4) is the keystone for both sides: svd2rust → an RT1176 PAC → the Embassy-class HAL foundation; and Renode ApplySVD → a named-register model for the hermetic HIL. One artifact unblocks the real-silicon HAL and the emulation, for M7 and M4.

The ask — get the ball rolling

Would gale treat "build-your-own OS" as a first-class mode, not just a side-effect of the standalone (plain/) track? Concretely, what we'd love to discuss:

1. A standalone runtime/construction crate — gale core + the minimal scaffold (boot/scheduler-init/device_init hooks) to compose an OS, no Zephyr.
2. The driver-framework backbone — are device_init / work / poll the right hooks to host the embedded-hal-async + kiln-async driver model, or should that be a thin new layer?
3. Positioning — does the "gale = composable OS components (drop-in or build-your-own), C-free" framing fit gale's roadmap? It changes the README story from "Zephyr primitives" to "OS components."

Cross-refs: gale#63 (host substrate epic), gale#65 (gust/gale-nano), and jess's DD-006 (maximal-wasm) / DD-011 (gust) / DD-017 (M7 = gale-maximal-wasm, no Zephyr in flight). No urgency — opening this to get the conversation started.

[avrabe]

And we should rethink thread and async handling together. As we hold both we can run an interesting dual track or merger or so. Research would be great and ideas to be seen. Especially we have to think here as wasm will give in addition corporative and someday real threads so we need to be prepared

[avrabe]

Took a first design pass at this — opened #75 with a tracked architecture (artifacts/byo_os.yaml, 12 artifacts) + a design doc (docs/byo-os-architecture.md, DOC-BYOOS-ARCH). Short version of the three asks:

1. First-class BYO-OS mode — yes. A construction crate = plain/ gale primitives + kiln-async + a reusable boot / scheduler-init / device_init scaffold (no Zephyr). gust is the reference minimal instance; this factors its hand-rolled superloop into hooks, so a new target is "pick components + provide the TCB shim".

2. device_init / work / poll — two yes, one no. device_init (bring-up ordering) and poll (waitable-set readiness; kiln-async's waitable-set/stream already echo k_poll) are the right reused verified hooks. work is not — kiln-async is the executor, so a workqueue on top duplicates it; deferred work is a task. The driver framework is a thin new layer anchored on embedded-hal-async, hosted on kiln-async, not routed through work.

3. Positioning — yes, and accurate. Both modes are proven: drop-in (36 QEMU suites + the wasm-dist sem/mutex/msgq modules) and build-your-own (gust on bare M3). The README story becomes "composable verified OS components — drop in, or build your own; C-free Rust+wasm."

The load-bearing design insight: the verification boundary maps exactly onto the wasm/native seam. Above embedded-hal-async = verifiable logic (relay decode + voting) → wasm (Kani + dissolved). Below = timing/DMA/privileged → the trusted, thin native substrate (Embassy-class HAL + the ~4-item boot shim). That's the same boundary gust drew for sync MMIO, generalised to async+DMA — the "full-fat gust seam" (DD-012/DD-015).

Honest carry-over: the async HAL substrate inherits gust's open rigor at async scale — native-substrate WCET (FIND-GUST-002), IRQ→waker concurrency proof (FIND-GUST-003), toolchain-TCB trust (FIND-GUST-004).

Cross-refs: #65 (gust), #63 (host substrate); jess DD-006/DD-011/DD-012/DD-015/DD-017. This is design-for-discussion — happy to iterate on the crate boundary and the device_init/poll hook shapes before any code.

[avrabe]

[jess — research on threads + async together, the dual-track/merger]

Did the deep-dive you asked for. Short version: don't merge — compose two already-verified schedulers as a clean dual track, and that same boundary is exactly what makes us wasm-threads-ready.

We already hold both halves (verified)

• Preemptive = gale's scheduler (src/sched.rs, proofs/lean/Scheduling.lean): Zephyr-faithful priority runq, should_preempt, SMP next_up_smp, and cooperative-thread semantics (SC6: coop threads not preempted except by MetaIRQ). Stackful.
• Cooperative = kiln-async: fuel-bounded stackless poll loop, Verus + Lean (RTA/EDF) proven.

So this is composition of two proven schedulers, not a from-scratch merge.

Recommended model: priority-banded hybrid (layered, not merged)

The Embassy/RTIC-proven shape, mapped to our verified pieces:

• gale preemptive threads = the priority backbone — hard-RT periodic + priority isolation + the MetaIRQ band.
• kiln-async executor(s) hosted inside a thread (one per priority band) — for the I/O-bound cooperative driver tasks, woken by the seam's DMA-completion IRQ→waker.
• jess mapping: falcon 1 kHz control = a high-prio gale thread (preemptive, deterministic WCET); failsafe = MetaIRQ/top; sensor drivers = kiln tasks in an I/O thread (cooperative, DMA-woken). This matches your gale#75 calls exactly (kiln is the executor; work is not a separate queue — deferred work is a task).

Why not merge into one scheduler: stackful-preemptive and stackless-cooperative are intrinsically different, each carries its own proof, and — crucially — merging would fight the wasm evolution below. Keep a clean dual track with a defined handoff (a gale thread hosts a kiln executor; preempt between bands, cooperate within).

Why this is the wasm-ready answer (your key concern)

The dual track maps 1:1 onto the wasm concurrency proposals, so the native→wasm migration is per-track and incremental — never blocked on one proposal:

our track (today, native/synth)	wasm proposal	status	migration
kiln cooperative (stackless poll)	stack-switching / typed continuations (WasmFX) — green threads, coroutines, async	phase 3	nearer-term: the cooperative track moves into wasm with real stacks, same role, same P3 async ABI
gale preemptive / parallel (SMP threads)	shared-everything-threads (real spawn + shared refs) + threads (shared mem)	phase 1 / phase 4, layering into the component model	longer-horizon: the preemptive track goes wasm-native

The load-bearing point: the component-model P3 async ABI is already the stable cooperative contract (kiln backs it today). When stack-switching lands, synth can lower that same ABI to wasm green threads instead of stackless polling — no API change. And the preemptive track rides shared-everything-threads-in-the-component-model when that matures. So "cooperative now, real threads someday" isn't a rewrite — it's two independent lowerings of contracts we already have.

M4 is the "real threads" case available now

M7+M4 over shared OCRAM is the shared-everything/SMP scenario — and gale's SMP scheduler already proves it (next_up_smp, SC9/SC10/SC11). So the preemptive-parallel track exists today at the native level (gale SMP across M7+M4, kiln-coop per core); it's the native preview of wasm shared-everything-threads. The dual track is therefore also the multi-core story, not just single-core.

Open rigor (extends your FIND-GUST-002/003/004 to the handoff)

The new surface is the coop↔preempt handoff (a gale thread hosting a kiln executor):

1. Priority-inversion bound — a cooperative kiln task must not block a higher-prio gale thread; provable given the executor thread's priority + yield-bounded (fuel-quantum) tasks. Worth a Lean lemma alongside Scheduling.lean.
2. IRQ→waker across the boundary — FIND-GUST-003 generalized: the seam IRQ wakes a kiln task inside a thread that may be preempted; the wake/ready handoff needs the concurrency proof at the preempt boundary, not just cooperative.
3. Combined WCET/schedulability — gale-preempt RTA + kiln fuel use the same exec unit (the kiln-async plan already parameterizes spar RTA/RMBound/EDF on it), so the hybrid is analyzable as one schedule. That's the proof that the dual track is hard-RT-sound.

Net idea: one component-model concurrency API; two verified schedulers behind it (gale-preempt + kiln-coop); two independent wasm lowerings (shared-everything-threads + stack-switching) as they mature. Happy to iterate — and to prototype the falcon-thread + kiln-driver-executor split on the M7 once the driver seam (embedded-hal-async, jess#62) firms up.

Sources: WebAssembly/stack-switching (phase 3, WasmFX), WebAssembly/shared-everything-threads (phase 1), WebAssembly/threads (phase 4), component-model Concurrency.md.

[avrabe]

Positioning update from two research sweeps (DOC-BYOOS-MARKET, DOC-WASM-FRONTIER in #75) — kept deliberately honest, then sharpened:

The honest part (don't pitch these as novel): the individual ingredients are prior art — import-boundary record-replay is Wasm-R3 (OOPSLA'24); "dissolve the runtime to native" ships in wasm2c/Firefox + w2c2; "wasm on MCU" is WAMR. We should adopt Wasm-R3's recorder and lead the debug story with divergence-localization (the verification-cut = the replay-cut → an identical-tape divergence provably excludes the verified logic), not "we invented record-replay."

The part the sweep underweighted, and we should NOT: the device class. WAMR — the universally-cited "wasm on MCU" — keeps a ~50–64 KB resident runtime; it structurally stops above gust's 8 KB / no-runtime / ~4-fn-TCB target. And nobody runs the Component Model on bare-metal MCUs at all. So "a CM-composed, wasm-authored OS, dissolved to native, on the sub-runtime device class" is genuinely unoccupied — and WAMR being the incumbent everyone points to strengthens this: the reference answer for wasm-on-MCU can't go where gale lives. (Tracked as FIND-BYOOS-005.)

Net intersection (defensible): verified app-functional-correctness carried through the dissolve to a runtime-free sub-WAMR MCU, as the same artifact across browser/host/HW, Component-Model-composed. Honest-prior-art and this uniqueness are not in tension — we hold both.

Tailwinds (external, real): EU CRA makes signed/attested OTA + SBOM a market-access requirement by Dec 2027; interpreted wasm is 10–50× native energy (the field concedes AOT is needed for battery) — both favour OTA-of-verified-dissolved-wasm for wohl (home automation, 2nd vertical). Espressif's ESP-LowCode split-firmware independently validates our import-seam cut.

The one gating move: finish the dissolved-native comparative bench (#21/#22) — every quantitative claim (beats WAMR-AOT, energy/flash win) needs the dissolved ARM artifact. It's close: the gust scout already dissolves the hot path to 812 B linkable Cortex-M3; the open gap is synth#383 (the 8 KB .bss link), not the old #167.

Live demo of the browser leg deploying via #76 → https://pulseengine.github.io/gale/