Design question: multi-memory → distinct native regions (MPU-protectable) vs single shared memory — which isolation model for the dissolved library-OS?

[avrabe]

Design question, not a bug — wanted synth's stance before gale commits an inter-component isolation model for the dissolved library-OS (gale#86, gale#89).

The two models

A dissolved image with multiple mutually-distrusting components needs memory isolation between them (verification stays the primary line; this is containment for the unverified/untrusted seam + 3rd-party components). Two shapes:

1. Single shared memory + MPU carving. What we do today: meld fuse --memory shared → one linear memory → synth lowers to one native region; the embedder/TCB carves MPU sub-regions per component by hand. Lowerable now, but the protection regions are bolted on, not structural.

2. Multi-memory → one native region per wasm memory. Keep each component in its own wasm memory; synth places memory[k] at a distinct native base, so the memory boundary is the MPU region boundary — protection is structural (the embedder just programs an MPU region per memory). Cleaner, but today synth loud-skips cross-memory ops (arm backend uses soft-float for all f32/f64 — hardware FPU never used (cortex-m4f/m7/m7dp identical); blocks REQ-PIX-001 hard-float #369) and there's no single-address-space lowering for multi-memory (meld#172).

The question for synth

Which model does synth want to be the supported MCU path?

• If multi-memory → per-region: would synth lower N memories to N native bases (region-relative addressing within each, cross-memory ops emitted explicitly rather than skipped), exposing the per-memory base/size so an embedder can map each to an MPU/PMP region? That makes "memory structure = protection structure" — arguably the right isolation primitive.
• If single-shared only: synth stays single-memory, and isolation is entirely the embedder's MPU-carving on one region (gale#86) — simpler backend, isolation regions hand-managed.

Why it matters / what we'll do with the answer

gale's BYO-OS isolation design (gale#86) forks on this. If synth intends multi-memory→region lowering, we'd pursue multi-memory ↔ MPU-region (structural). If not, we commit to shared + MPU-carve. Either is fine — we just shouldn't build against an assumption synth doesn't hold.

Kill-criterion for "we picked the right one"

"The chosen model can give per-component MPU-enforced isolation on an M-class MCU after dissolve, with region boundaries that don't require hand-maintained address maps." Refs: synth#369 (cross-memory loud-skip), meld#172, gale#86, gale#89.

[avrabe]

[synth maintainer side — issue-hunt triage] Good question to settle before gale#86 commits. Short version: the model choice is meld's, not synth's — synth lowers the memory structure it's handed (meld fuse → loom → synth; whether the dissolved image carries one memory or N is decided at fusion, meld#172). So let me answer for synth's layer rather than pick the model for the whole pipeline.

Today: synth is single-memory. The lowerable MCU path is meld's --memory shared → one linear memory → one native region at a fixed base (R11). Model 2 isn't deliverable end-to-end yet: synth drops the memory index at the IR level and loud-skips cross-memory memory.copy/memory.fill (#369), and MPU is currently config-only — region tables computed, but no runtime enforcement wired into the optimized codegen path (#377).

Synth will not be the blocker for model 2. When meld#172 emits multi-memory, synth's part is concrete and stageable:

• carry memidx through the IR instead of dropping it;
• place each wasm memory at a distinct native base;
• emit cross-memory ops explicitly (closing arm backend uses soft-float for all f32/f64 — hardware FPU never used (cortex-m4f/m7/m7dp identical); blocks REQ-PIX-001 hard-float #369);
• expose per-memory base/size (the MPU region machinery already computes base/size/permissions) so the embedder programs one MPU/PMP region per memory.

The latent infra (synth_memory::MemoryTable, MAX_MEMORIES=8; the MPU region allocator) is a starting point, not "close" — the hot-path addressing (per-memory base, cross-memory access) and the #377 MPU runtime wiring are the real unbuilt work.

On the isolation merits: model 2's advantage isn't "no address maps" — both models propagate a layout (model 1 from meld's carve, model 2 from the per-memory bases). It's that protection boundaries coincide with semantic boundaries: under model 2 a component can't even form a pointer into a neighbor (different native base); under model 1 a miscomputed address lands in a neighbor's sub-range and only the MPU catches it (defense-in-depth, but the error is expressible). The MPU/PMP region cap (~8 on ARMv7-M, PMP similar) applies to both, so it's not a differentiator — and it does cap practical N either way.

Synth's lean: model 2 is the better isolation primitive where you need true mutual-distrust containment; model 1 is the correct lowerable-today fallback. The pick is a joint meld+synth call gated on meld#172 + the synth multi-memory work + #377 MPU wiring — happy to sequence the synth side once meld commits the fusion direction. Refs: #369 (cross-memory loud-skip), #377 (MPU not runtime-enforced on the optimized path), meld#172.

[avrabe]

Looped meld in at meld#300 — since the fusion-structure decision (preserve N memories vs fuse to one) is meld's, the isolation-model fork can't be settled without them. meld's current thrust is --memory shared (meld#298/#299); meld#300 asks whether that's the committed dissolved-MCU path or whether meld intends a memory-preserving fuse mode for structural isolation.