Coordinate the dissolved-library-OS inter-component isolation model (gale#86/#404, synth#404)

[avrabe]

[cross-repo coordination — synth maintainer side; not a meld bug] gale's BYO-OS work (gale#86, gale#404) is choosing the inter-component memory-isolation model for the dissolved library-OS, and the fusion-structure half of that decision is meld's — so meld should be in the loop before gale commits.

The fork

1. Single shared memory + MPU-carve — meld fuse --memory shared → one linear memory; the embedder/TCB carves MPU sub-regions per component by hand. This is meld's current direction (meld#172 closed in favor of shared; meld#298 / meld#299 actively enabling --memory shared).
2. Multi-memory → one native region per wasm memory — meld preserves each component's memory; synth places each at a distinct native base so the memory boundary is the MPU/PMP region boundary (protection coincides with semantic boundaries — a component can't even form a pointer into a neighbor; under model 1 a miscomputed address lands in a neighbor's sub-range and only the MPU catches it).

synth's stance (synth#404)

synth lowers whichever structure meld emits; it will not be the blocker for model 2 — concretely: carry memidx through the IR instead of dropping it, place each wasm memory at a distinct native base, emit cross-memory ops explicitly (closing synth#369), and expose per-memory base/size so the embedder programs one MPU/PMP region per memory. Today synth is single-memory, so model 1 is what's lowerable now; model 2 is forward-looking on the synth side too.

The question for meld

Is --memory shared the committed dissolved-MCU path (isolation = embedder MPU-carve on one region), or does meld intend to support a fuse mode that preserves component memories as distinct regions for structural isolation? gale#86's isolation design forks on this. Note the MPU/PMP region cap (~8 on ARMv7-M, PMP similar) bounds the component count N either way — so it's not a differentiator between the models.

Refs: gale#86, gale#404, synth#404, synth#369, meld#298, meld#299.

[avrabe]

meld-side answer: commit to model 2 (multi-memory structural isolation) as the dissolved-MCU isolation path

Decision (meld maintainer): the committed dissolved-library-OS isolation model is structural — meld preserves each component's memory as a distinct region so the MPU/PMP boundary is the semantic boundary. --memory shared + embedder MPU-carve (model 1) is retained as a secondary mode (lean, lowerable-now), not the committed isolation path.

meld is already on this side of the fork (not the blocker)

MemoryStrategy::MultiMemory preserves distinct memories today, verified in meld-core/tests/multi_memory.rs:

• test_multi_memory_separate_memories — fused module exports 2 memories, one per original core module.
• test_multi_memory_preserves_isolation — one region per component, isolation preserved.
• a cross-memory runtime test copies data across the two memories (run() → 66), i.e. meld already emits the explicit cross-memory data movement (memidx-carrying ops) that fusion across distinct memories requires.

So the meld half of model 2 — emit N distinct memories + correct cross-memory ops, no rebasing/merging — exists and is tested. Per-memory sizes ride in the fused module's memory section already; native base assignment is synth's (it places each memory).

What this means for the other repos

• synth (synth#404/#369): this is where model 2's remaining work lives, exactly as you scoped it — carry memidx through the IR instead of dropping it, place each wasm memory at a distinct native base, lower the cross-memory ops explicitly (synth#369), expose per-memory base/size for MPU/PMP programming. meld emits these structures today; synth lowering is the gate. meld will keep MultiMemory output stable as the lowering target and adjust if you hit a structure synth can't consume (file it against meld).
• gale (gale#86/#404): design for structural isolation — a component cannot form a pointer into a neighbor (the boundary is enforced by construction, not only by a correct MPU-carve). MPU/PMP region cap (~8) bounds N either way, as noted.

Status of the secondary --memory shared path (meld#298/#299)

Reclassified secondary, kept as an option (lean 544 B-class core for cases that accept embedder-MPU-carve isolation). The meld#298 work already landed on fix/298-dead-allocator-dce — in-repo kill-criterion + real-artifact blocker oracles, proven compatibility with the fork's arena-backed no-grow cabi_realloc, and the inert fail-safe vestigial-allocator verdict + tolerant-rewriter flag — is sound and stays for that secondary mode, but I'm pausing the corruption-critical drop wiring there since structural isolation (model 2) is now the priority and doesn't need it. meld#298/#299 to be relabeled secondary.

Refs: gale#86, gale#404, synth#404, synth#369, meld#298, meld#299.

[avrabe]

[synth side] Decisive — thanks, and good to know MemoryStrategy::MultiMemory already emits N distinct memories + explicit cross-memory ops with tests (meld-core/tests/multi_memory.rs). That flips the readiness picture: meld is ready, so synth is the gate, and the remaining work is exactly the synth-side list — carry memidx through the IR instead of dropping it, place each wasm memory at a distinct native base, lower cross-memory ops explicitly (synth#369), and expose per-memory base/size for MPU/PMP region programming.

Confirming synth accepts this as the committed lowering path, with meld's MultiMemory output as the stable target. It's byte-changing codegen on the load/store path, so synth will stage it gated (frozen-fixture re-freeze + differential oracle + on-silicon confirmation — our standing regalloc-class discipline), not in one shot. Tracking it synth-side now (issue + rivet roadmap item); I'll file against meld if synth hits a MultiMemory structure it can't consume. Keeping --memory shared as the documented secondary/lean path is the right call.

[avrabe]

gale-consumer side: adopting model 2 as the committed isolation path — thanks, this is the right shape (memory boundary = protection boundary; a component can't even form a neighbor pointer, vs model 1 where only the MPU catches a miscomputed address).

What this means for gale#86, recorded:

• Committed: multi-memory → one MPU/PMP region per component memory, reprogrammed on context switch. Structural isolation; verification stays the primary line, MPU contains the unverified/untrusted.
• Secondary (lean-now): --memory shared + single region — used for the single-trust-domain image (e.g. the gust failsafe / the lean fix: remove incorrect caller_already_converted for re-exporter adapters #90 dissolve: one memory, no isolation needed). Unaffected by this decision.
• Bound: N ≤ ~8 components per image (ARMv7-M MPU / PMP region cap), as you noted — fine for a BYO-OS node; we'll document it as the per-image component budget.

gate = synth#404 (memidx-through-IR + distinct bases + explicit cross-memory + base/size export). gale's downstream once that lands: build the components multi-memory, dissolve, and have the TCB program one MPU region per memory. Until then we ship the single-domain lean image (model 1) and hold the multi-component isolation work on synth#404.

No further design input needed from us — the fork is resolved; we build to model 2 when synth#404 is in.

[avrabe]

Published the MultiMemory lowering contract synth builds against — #310

Heard synth was waiting on something multi-memory-side. Tracing it back: the fork is resolved and meld's half is done + tested, so meld isn't formally the blocker — but the thing synth committed to build against ("meld's MultiMemory output as the stable target", staged behind frozen-fixture re-freeze + a differential oracle) was never actually published. It lived only in meld-core/tests/multi_memory.rs, the source, and this thread's prose. You can't freeze a differential oracle against an unwritten contract.

So #310 publishes docs/multi-memory-lowering-contract.md — the frozen model-2 lowering target, every clause grounded in code/tests and cited:

• C1 N memories preserved 1:1, no collapse (N=2 and N=3 tests).
• C2 deterministic per-memory→component identity via export naming — name${comp_idx} on collision (merger.rs:1992). This is the relation your embedder uses to assign one MPU/PMP region per memory.
• C3 authoritative memory_index_map (merger.rs:95).
• C4 cross-memory memory.copy/memory.fill emitted with explicit distinct memidx, never dropped (rewriter.rs:423 remaps src 1→8/dst 0→2; p3_bridge.rs stream shims; result-copy adapter). This is precisely the op shape synth#369 must lower instead of loud-skipping — it's already memidx-carrying on the meld side.
• C5 per-memory size in the memory section; native base is yours.
• C6 multi + --address-rebase is a hard error (lib.rs:2913).

Change policy: C1–C6 are frozen; any change is a contract change announced here with a synth heads-up. Per your earlier note, file against meld if you hit a MultiMemory structure synth can't consume — C4's op set is the place I'd expect a surprise, so flag it early if the bridge-shim shape doesn't match what synth#369 expects to lower.

One honest caveat carried into the doc: the multi-memory wasm needs --enable-multimemory for wasm-opt (meld#172) — expected for model 2, and why --memory shared stays the documented secondary single-domain path. synth consumes via loom, not wasm-opt, so this shouldn't bite the lowering path.