SSA without Dominance for Higher-Order Programs
summary
Dominance is replaced by a data-flow notion of free-variable nesting tree that applies to higher-order, scopeless IRs; nesting implies (but is strictly stronger than) classic dominance and is mechanized in Lean. Implementation in the Mimir compiler provides an incremental free-variable analysis with cached, invalidated results and demonstrates n log n scaling on real benchmarks; practical artifacts and evaluated code are available, and beta-reduction becomes the mechanism for inlining, loop peeling and unrolling.
AI-written summary · about
chapters (18)
- 0:00SSA and dominance limits
- 1:05Dominance in nested loops
- 2:29Higher-order dominance breaks
- 3:53Syntax trees vs scoping
- 5:15CFG and SSA limits
- 5:57Lambda graph for higher-order
- 7:03SSA to lambda graph in CPS
- 8:50Free variable replaces dominance
- 10:37Free variable analysis benefits
- 11:42Beta reduction without blocks
- 12:24Nesting tree vs dominator tree
- 13:28Lambda graph beyond CPS
- 14:12Lambda graph performance
- 14:56CFG-SSA to lambda graph
- 16:01Nesting vs dominance takeaways
- 16:44Q&A on proofs and MLIR
- 17:26MLIR block arguments
- 18:31De Bruijn indices
related talks
18mSSA is Freyd Categories
18mGraph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Af...
28mSSA CFG Yul A new viaIR backend
29mA Flow-Insensitive-Complete Program Representation
14mHigher-Order Demand-Driven Symbolic Evaluation
23mAn Abstract Interpretation for SPMD Divergence on Reducible Control Flow Graphs
18mCompiling with Abstract Interpretation
26mSSA Translation Is an Abstract Interpretation