Verifying term graph optimizations using Isabelle/HOL
summary
Formal verification of hundreds of GraalVM expression optimizations proceeds by extracting maximally shared subgraphs into terms and lifting term rewriting refinement proofs back to graphs, using Isabelle/HOL to discharge obligations. A small set of five optimizations drops proof effort from 58 lines to 3 lines by automating refinement and a per-phase termination check; a Java-like DSL generates refinement and termination goals from the compiler’s Sea of Nodes IR. Works for side-effect-free expressions; memory and effectful rules remain manual and future work.
AI-written summary · about
chapters (8)
- 0:00Start
- 1:45Partial evaluation
- 7:32Theory vs Practice
- 8:08Sharing common sub-expressions
- 10:04Term graph to term
- 10:23Expression semantics
- 10:35Expression refinement
- 10:56Term graph semantics preservation
related talks
15mVerifying and Improving Halide’s Term Rewriting System with Program Synthesis
37mA Tour of Program Optimization
46mRefinement Types from Light to Deep Verification
23mFormally Verified Speculation and Deoptimization in a JIT Compiler
34mLiquid Haskell: Verification with Refinement Types
19mAutomated Verification of Fundamental Algebraic Laws
18mGraph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Af...
01h 06mVerifying a compiler through equational means