D-507 phase 3: bounds-check elision flip + AOT soundness guard (ADR-0202 D4/D5) — completes D-507#133
Merged
Merged
Conversation
…ies (ADR-0202 D4/D5, D-507) Both emit backends gain `bounds_elided`: when memory0 qualifies (i32 × 64 KiB × guarded host) AND the engine knob is `.auto`, memory0 scalar/ atomic accesses drop the inline ADD/CMP/B.HI (x86_64: mem_limit reload + CMP + JA) — the guard-page reservation + fault→trap redirect own oob detection — and force-emit the kind=6 stub as the redirect target. memory64 / bulk / GC-array / SIMD keep explicit checks (SIMD = D-514). Atomic alignment checks are NOT elided. The elision decision uses the SAME memory_backing.qualifies predicate as the runtime backing choice, so elided code only ever binds guarded memory0 (D5 soundness by construction). Engine knob `bounds_checks: .auto|.explicit` (compile.setBoundsChecks, process-global to avoid threading 56 compileWasm callers) — the D-510 differential axis. Any JIT execution now auto-installs the fault handler (entry.invokeAndCheck → signal.ensureInstalled, idempotent, skips when CLI/embedding/spec-runner already installed one) since elided code faults instead of branching. The spec harness backs memory with non-guarded buffers, so it forces .explicit (D-515 tracks running the corpus under elision). New test-oob-elision build step verifies the full production path (guarded memory + elided codegen + guard fault → redirect → trap → exit 1) per-OS.
…s the hypothesis Per-merge bench (arm64) + ADR V-phase note: memory0 scalar bounds-check elision is ~noise on the shootout band (matrix ~1%, base64 ~1.5%, sieve ~4%, fib2 within stddev), NOT the '1.75x floor slice' the ADR Context hypothesised. The check was a pinned-reg CMP + never-taken branch — cheap on OoO; the real 1.75-3.9x gap vs wasmtime is optimising-tier codegen quality (D-513). Elision still ships (correct, code-size win, standard design, D-509-foundational guard-fault infra), but the perf hypothesis is recorded as refuted per the measure-first principle.
…ole (ADR-0202 D5, D-507) Adversarial critique FAIL #5 (CONFIRMED memory-safety regression): the AOT compile path used the default .auto knob → elided .cwasm code, but aot/run.zig binds PLAIN HEAP with no trap region → an oob access reads/ writes past the guest memory silently; reproduced as compile+run oob.cwasm → exit 70 (JIT path cleanly traps exit 1). Enforcement: CompiledWasm.bounds_elided + produceFromCompiledWasm HARD-REFUSES elided (Error.ElidedBoundsNotAotSerializable); compileWasmForAot forces .explicit for every AOT compile; regression test pins it. FAIL #6: the three bespoke-memory spec runners now force .explicit. D-515 tracks the D5 AOT-elision build-out + corpus-under-elision. test-all + lint green.
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.
Summary
Final phase of D-507 (ADR-0202 D4/D5), on top of phase 1 (#131) + phase 2
(#132). Flips on memory0 scalar bounds-check elision for guard-page-qualifying
memories, behind an
.auto/.explicitknob, with a hard AOT soundness guard.Completes D-507.
Elision (D4)
bounds_elided: when memory0 qualifies (i32 × 64 KiB× guarded host) AND the knob is
.auto, memory0 scalar/atomic accesses dropthe inline
ADD/CMP/B.HI(x86_64: mem_limit reload + CMP + JA); the kind=6stub is force-emitted as the guard-fault redirect target. memory64 / bulk /
GC-array / SIMD keep explicit checks (SIMD = follow-up D-514); atomic
alignment checks are never elided.
memory_backing.qualifiespredicate asthe runtime backing choice → elided code only ever binds guarded memory
(D5 binding-time soundness by construction).
entry.invokeAndCheck→signal.ensureInstalled, idempotent).bounds_checks: .auto|.explicit(runner.setBoundsChecks) — the D-510differential axis.
AOT soundness guard (D5) — closes a confirmed memory-safety hole
An adversarial review found that the AOT
.cwasmpath compiled.auto(elided) but
aot/run.zigbinds plain heap with no trap region → an oobaccess would read/write past the guest memory silently (sandbox escape).
Fixed structurally:
CompiledWasm.bounds_elided+produceFromCompiledWasmhard-refuses an elided module (
ElidedBoundsNotAotSerializable);compileWasmForAotforces.explicitfor every AOT compile. The threebespoke-non-guarded-memory spec runners force
.explicittoo. Regression testpins the refusal. Full D5 AOT-elision build-out tracked as D-515.
Measured perf (retrospective — hypothesis refuted, recorded honestly)
The ADR framed elision as "the biggest tier-free lever (1.75–3.9x band)". The
arm64 shootout delta is ~noise: matrix ~1%, base64 ~1.5%, sieve ~4%, fib2
within the ±2–4% run stddev. The check was a pinned-reg CMP + a well-predicted
never-taken branch — cheap on OoO. The real 1.75–3.9x gap vs wasmtime is
optimising-tier codegen quality (D-513), not bounds checks. The elision still
ships: correct, code-size win, standard production design, and its guard-fault
machinery is the reusable foundation D-509 (threads = base-stable memory)
needs.
Verification
zig build test/test-all/lint --max-warnings 0green.test-oob-elisionbuild step (all 3 OSes via test-all):zwasm run --engine jiton a boundary oob load → guard fault → redirect → trap → exit 1.runner_trap_test); AOT-refuses-elided regression test.
latent spec-runner breach both fixed in-branch; the JIT elision itself passed
every soundness probe.
Refs: D-507 (completes) · ADR-0202 D4/D5 · D-514 (SIMD elision) · D-515 (AOT
elision build-out + corpus-under-elision) · D-513 (optimising-tier decision)