Semantics Lifting for Scientific Kernels
summary
Claims an automated pipeline that recovers mathematical specification from C kernels by reversing SPIRAL’s codegen passes, using clang to AST, reparsing to SPIRAL IR, normalizing loop gather-compute-scatter patterns, and applying existing rewrite rules. Prototype lifts recursive and loop FFTs, recognizes Cooley-Tukey DFT structure, and detects semantic bugs (e.g., index changes) on GPT-generated FFT code. Limits include data-dependent computations and algorithms unknown to SPIRAL’s knowledge base.
AI-written summary · about
chapters (12)
- 0:00Semantics lifting research
- 1:28Semantic correctness challenge
- 2:31Semantics lifting as decompilation
- 3:55Spiral’s rewrite rules for lifting
- 5:17Partial lifting: limits and value
- 6:22Legacy code and future use
- 7:04Q&A: recursion and system
- 8:08Q&A: lifting system design
- 9:11Q&A: math foundations
- 9:32Q&A: existing vs new
- 9:52Q&A: compiler optimization
- 10:12Q&A: debugging and legacy
related talks
17mTowards Semantics Lifting for Scientific Computing: A Case Study on FFT
14mVerification of Algorithm and Code Generation for Signal Transforms- 14mVerification of Algorithm and Code Generation for Signal Transforms
16mSemiring Optimizations: Dynamic Elision of Expressions with Identity and Absorbing Elements
31mProgramming Languages Must Have Formal Semantics. Period.
19mCompiling Recurrences over Dense and Sparse Arrays
01h 05mAll the Languages Together
19mSpEQ: Translation of Sparse Codes using Equivalences