Experience Report: Stack Switching in Wasm SpecTec
summary
Implements the STX stack‑switching extension in SpecTec by encoding captured continuations as lists of frames and using a bubbling semantics that escales frames one by one. Finds that naive bubbling produces a lot of duplicated rules so SpecTec generates match functions (extraction functions) per context to locate labels and captured values. Proposes adding native context to SpecTec to avoid repetition, notes several backend and DSL changes are required and the current solution is fragile.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:07Stack switching in SpecTec
- 2:14WebAssembly semantics
- 6:17Frames and control structures
- 8:24Stack switching semantics
- 10:16Bubbling implementation
- 12:47Contexts in semantics
- 14:55Native context design
- 17:07Match functions
- 20:00Implementation challenges
- 21:17Q&A
related talks
47mStack Switching in WebAssembly with Effect Handlers
16mBringing the WebAssembly Standard up to Speed with SpecTec
26mSpecTec, a Single Source of Truth
47m[Keynote] Keynote and SpecTec demo
18mSuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT(…)
25mP4-SpecTec: A Language Mechanization Framework for P4
35mStrongly-Typed Multi-View Stack-Based Computations
19mIris-WasmFX: Modular Reasoning for Wasm Stack Switching