Indexed Types for a Statically Safe WebAssembly
summary
Wasm-prechk extends Wasmtime with an indexed-type system and a new memory-load-precheck instruction that lets the compiler remove per-access dynamic bounds checks; it implements constraint solving during typing and runs on PolyBenchC, yielding 1.71x average runtime speedup, ~7.18% larger binaries and ~1.4% slower type-checking. The implementation ships as a Wasmtime extension, comes with artifacts, and the authors prove type- and memory-safety, backward compatibility, and type-erasure to Wasm.
AI-written summary · about
chapters (10)
- 0:00Indexed types for Wasm
- 1:26Dynamic checks inefficiency
- 2:31Wasm Pre-Check for static safety
- 3:53Dynamic checks in Wasm code
- 7:08Extending Wasm type system
- 9:13Replacing dynamic checks
- 12:26Performance gains from static safety
- 14:31Overhead and practical considerations
- 15:15Future work and type inference
- 15:37Q&A
related talks
26mMemory Safety Preservation for WebAssembly
22mThe state of WebAssembly
19mUpdating WasmCert-Isabelle to WebAssembly 2.0
01h 08mOn WebAssembly
37mBuilding a better web with WebAssembly at the edge
39mFast future with WebAssembly
32mAll The Memory Safety Of C Combined With All The Blazing Speed Of JavaScript
43mMeet Your Future - WebAssembly