HEC: Equivalence Verification Checking for Code Transformation via Equality...
summary
HEC introduces a concrete equivalence checker that leverages an e-graph backend on MLIR, combining over 60 static rewrite rules with generated dynamic rewrite rules checked by three SMT solvers to handle both datapath and control‑flow transforms. It verifies loop unrolling, tiling, fusion across PolyBenchC, processes ~100,000 lines of MLIR in ~40 minutes, and finds two real mlir-opt bugs: a loop boundary check that causes extra executions during unrolling and a read‑after‑write violation from loop fusion. HEC PolyBenchC
AI-written summary · about
chapters (14)
- 0:00HEC introduction
- 1:02Compiler verification challenges
- 2:26Data/control flow examples
- 3:53Limitations of tools
- 4:59Egraphs in equivalence
- 6:03HEC framework
- 7:27Static data rewriting
- 8:52Dynamic control rules
- 9:56Loop tiling rules
- 10:18Egraph verification process
- 11:20Formal guarantees
- 12:04Experimental results
- 13:51MR compiler bug
- 14:54Q&A
related talks
21mChecking Equivalence in a Non-strict Language
19meqsat: An Equality Saturation Dialect for Non-destructive Rewriting
01h 06mVerifying a compiler through equational means
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
22mAlgorithm-Aware Hardware Optimization using E-Graph Rewriting: how should we marry(…)
34mLiquid Haskell: Verification with Refinement Types
30mAutomated High-Level Synthesis Design Modularization via E-Graph Anti-Unification
17mBetter Together: Unifying Datalog and Equality Saturation