An Abstract Interpretation for SPMD Divergence on Reducible Control Flow Graphs
summary
Presents an abstract interpretation for uniformity that handles reducible CFGs, with a largely Coq mechanized proof of correctness and an LLVM prototype implementation. Claims precision matches LLVM’s default divergence analysis while being sound on more general CFGs, and measures show it is faster and more precise than a state‑of‑the‑art non‑interference analysis, giving across‑benchmarks compile‑time parity and up to ~5% improvement in vectorized code performance.
AI-written summary · about
chapters (6)
- 0:00SPMD divergence analysis intro
- 3:46Reducible CFG challenges
- 8:10Abstract interpretation overview
- 13:00Concrete vs abstract domains
- 17:25Applications and case studies
- 22:09Benchmarking performance
related talks
16mAutomatically Deriving Control-Flow Graph Generators from Operational Semantics
18mCompiling with Abstract Interpretation
27mPartial Evaluation of Reversible Flowchart Programs
21mFlow-Analysis-Based Closure Optimization
27mTaming Unsoundness with Gradual Abstract Interpretation
46mMechanizing Abstract Interpretation
17mDenotation-based Compositional Compiler Verification
19mCompiling Probabilistic Programs for Variable Elimination with Information Flow