First-Class Verification Dialects for MLIR
summary
Adds semantics as first-class MLIR dialects and a pipeline that lowers compiler IRs through high-level memory and undefined-behavior dialects to an SMT dialect, implements a state-of-the-art SMT encoding for memory, and provides dialect-agnostic tools: translation validation, canonicalization verification, and dataflow-transfer verification. Evaluation finds five miscompilation bugs, verifies a canonicalization pass, proves transfer functions for known-bits and demanded-bits and shows the verified transfer functions detect 36.6% more known bits on average; SMT optimizations yield 60% Z3 speedup.
AI-written summary · about
chapters (9)
- 0:00MLIR and dialects intro
- 1:27Dialect semantics challenges
- 2:53Semantics dialect intro
- 4:39Compiler and SMT roles
- 7:06High-level semantics
- 8:34Lowering to SMT-LIB
- 10:37Tools with semantic dialects
- 13:25Conclusion and future
- 14:29Q&A
related talks
14mSound and Modular Activity Analysis for Automatic Differentiation in MLIR
11mEnabling Composition of Kernels and Compilers
59mVerification and Machine Learning
18mA Verified Compiler for a Functional Tensor Language
12mLanguage-Model Probabilistic Programming for Improving Autoformalization via Cycle(…)
34mOptimizing AI Inference with ML Compilers & Hardware
15mScaling Optimization Over Uncertainty via Compilation
38mFireside chat