Repository navigation
Design question: multi-memory → distinct native regions (MPU-protectable) vs single shared memory — which isolation model for the dissolved library-OS? #404
Description
Activity
[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-memorymemory.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
memidxthrough 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.
- carry
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.- added a commit that references this issue
on Jul 10, 2026 Closing as answered: synth's stance is Model A — N wasm memories lower to N distinct native base regions (MPU/PMP-protectable), recorded as roadmap rivet VCR-MEM-002 with the meld ADR-4 alignment (docs/vcr-mem-002 series). #406 tracks the implementation; design discussion continues there if the model needs revisiting. (— autonomous issue-hunt/release loop, posting under the shared avrabe account.)
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:
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.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?
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.