Scaling Instruction-Selection Verification against Authoritative ISA Semantics
summary
Arrival verifies Cranelift instruction selection end to end by composing rules (rule chaining) and auto‑deriving ISA specs from vendor ASL via a symbolic‑encoding pipeline, verifying nearly all AArch64 rules used for Wasm core (over 6,000 rule chains), cutting developer effort so 60% of nodes need no handwritten spec and requiring 2.6X fewer hand specs, catching real bugs (a signed‑division error spanning 12 rules and seven ISA families), and running as an 11‑minute CI run using an SMT‑based verifier.
AI-written summary · about
chapters (11)
- 0:00Verifying instruction selectors
- 1:04Instruction selection in compilers
- 2:49Scaling verification challenges
- 3:54Arrival verifier and its core techniques
- 4:36How CraneLift achieves selection
- 6:02Rule chaining for specifications
- 7:46Automating ISA specifications
- 9:31Specifications for symbolic code
- 10:35Verification results and CI
- 11:38Catching signed division bugs
- 12:21Q&A
related talks
12mISA Formal Task Group Update
36mTowards a Formally-verified Software Toolchain for open ISAs
09mBreaking the RISC-V Processor Customization Barrier with Formal Verification
26mArchSem: Reusable Rigorous Semantics of Relaxed Architectures
02h 49mA Tour of the RISC V ISA Formal Specification
16mThe Morello ISA semantics, proof, and test generation
09mSemi-Automated Translation of a Formal ISA Specification to Hardware
40mFull-Stack Correctness in Wasm: Eliminating Bugs Inside and Outside the Sandbox