Repository navigation
feat(gust): one scheduler, one clock — spawn and timer import instead of embedding - #236
Merged
Merged
Conversation
…e (gale#224) One wasm component exporting all five gust:os capabilities (time, log, spawn, exec, timer) whose only residual imports are gust:hal/mmio and the app-supplied gust:os/taskdisp. 16905 B, validates, gated by build-fused-gustos.sh. wac plug does not apply: the five providers are a flat antichain (no provider consumes another's export), so every plug ordering exits "the socket component had no matching imports for the plugs that were provided". The operation needed is a union merge with import forwarding — wac compose over a WAC script. build-gustos-components.sh now builds all five providers, and its per-component gate is widened from "imports only gust:hal/*" to "imports only gust:hal/* or gust:os/*" — exec-provider and spawn-provider legitimately import the trusted gust:os/taskdisp dispatch, which the APPLICATION supplies, so it is expected to survive composition. Negative-tested: env, wasi:*, and heap imports still fail. Not lowered to native, not run anywhere, and the three embedded executor copies remain three separate Tasks tables in three separate linear memories — the composite is structurally fused but semantically triplicated. FUSED-GUSTOS.md records all of this explicitly. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…mer stateless (gale#224) exec/spawn/timer-provider each #[path]-included plain/src/executor.rs and each kept its own `static mut TASKS`. Composed, that was three component instances with three scheduler states, so a handle from spawn.start() was meaningless to timer.sleep() and exec.state() — while wit-os/gust-os.wit's timer.sleep doc already called its argument "the handle the app holds from spawn.start". The WIT specified a shared handle space the implementation did not provide. Separately, timer-provider and time-provider each hardcoded TIM2_CNT = 0x4000_0024 and read it independently: one clock only because two constants matched. A provider must import every capability it does not own: exec owns the executor imports taskdisp exports exec + sched/tasks spawn owns nothing imports sched/tasks exports spawn timer owns nothing imports sched/tasks + time exports timer time owns the clock imports hal/mmio exports time log — imports hal/mmio exports log New WIT package gust:sched@0.1.0 (wit-os/deps/sched) holds the internal seam, deliberately outside gust:os: composition satisfies it in place, so it never appears in the fused component's world and a tenant importing gust:os has no name to bind scheduler mutation to. spawn and timer are now stateless — no static mut, no mapping table; a spawn handle IS the executor's handle. timer has no gust:hal import at all. plain/src/executor.rs is untouched (Verus/Kani). Gates: - build-gustos-components.sh: allows gust:sched per-provider, and gates at source that exactly one crate #[path]-includes the executor. - build-fused-gustos.sh: residual imports EXACTLY gust:hal/mmio + gust:os/taskdisp (gust:sched must not leak), with an in-band negative test that composes the same five components unwired and requires the identical check to reject it; plus a one-scheduler gate that unbundles the composite and asserts one dispatcher and that spawn's and timer's scheduler operations both route to it. - Rejected signal, recorded in FUSED-GUSTOS.md: searching each core module for the executor's source path is NOT a detector — rebuilt from HEAD, neither pre-change provider module contains it (bounds checks elided) though both held a table. - build-os-ts.sh: exec-provider joins the node and the composition moves from wac plug to wac compose (plug never wires plug->plug, so the spawn->exec edge has to be named). Verified end-to-end to a temp OSNODE: 7836 B / 8192. Composite: 20741 B, 5 exports, residuals mmio + taskdisp. Still 5 linear memories at 1/17/17/1/17 pages — unchanged, and not the defect: the CM is shared-nothing and every instance gets its own. No memory-count reduction is claimed. Checked-in *.o were deliberately not regenerated. gust_exec_probe and gust_timer_probe still pass (both exercise the executor natively, so they confirm no regression rather than exercising the new composition). Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…e-clock # Conflicts: # benches/gust/drivers/FUSED-GUSTOS.md # benches/gust/drivers/build-fused-gustos.sh # benches/gust/drivers/build-gustos-components.sh
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes the defect #235 surfaced: the composite exported
gust:oscorrectly while containing three schedulers and two clocks.Principle: a provider must import every capability it does not own.
gust:os/taskdispgust:os/exec+gust:sched/tasksgust:sched/tasksgust:os/spawngust:sched/tasks,gust:os/timegust:os/timergust:hal/mmiogust:os/timeplain/src/executor.rsis untouched — it stays in exec-provider with its proofs; spawn and timer lost their#[path]includes and all statics.The composite is sealed
No
gust:schedanywhere. That was the reason for putting the scheduler seam in its own package rather than wideninggust:os: a downstream tenant importing the published, signed world cannot reachset-deadlineand mutate scheduling state. 20 741 B (was 16 905; the delta is exec's second exported interface and its WIT type section).One scheduler, verified by routing
Exactly one module owns dispatch and imports no
gust:sched; spawn and timer route their scheduler operations to it. A provider with a private table would do those locally and not import them.A gate was written, disproved, and thrown away
The first ownership check searched each core module for
plain/src/executor.rs(rustc bakes it into bounds-check panic locations). It is not a detector: rebuilding the pre-change spawn and timer providers showed neither module contains that string — both bounds-check before indexing, so the panic path is elided — while both held a full privateTasks. That gate would have printed "exactly one" over the triplicated composite. ATaskslives in wasm.bss, which a module never declares, so there is no binary signal for "holds a table".Replaced with two decidable checks: source-level (only one crate may
#[path]-include the executor) and composite-level routing (above). Negative-tested against the pre-change providers — it fires on all three signals.The residual-import negative test runs in-band on every invocation: the script composes the same five components with an unwired script and requires the same function to reject it.
wac plugnow works — and still cannot build thisThe edges are real now, and
wac plug timer-provider --plug exec-provider --plug time-providersucceeds where every pre-change ordering failed. It still can't produce the deliverable: a plug result exports only the socket's exports, and plug never wires plug→plug, sogust:sched/tasksgoes unsatisfied. Sowac compose— but the script now names real edges instead of a bare{ ... }union.Not claimed
spawn.start()and observed the handle intimer.sleep()through this composite. The two qemu probes exercise the executor natively and confirm no regression, not the new wiring.spawn-provider-cm3.o,timer-provider-cm3.oandos-ts-cm3.oare deliberately not regenerated; standalone re-measurements recorded in the RESULTS files (spawn text 1108→376, timer 844→552).timer-provider/RESULTS.mdsaidsleepwas blocked on synth#518. Measured pre- and post-change at synth 0.49.0 — both compile 5/5. That text described an olderticks: u64WIT; this change did not fix it, and the file now says so.🤖 Generated with Claude Code
https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo