Towards Semantics Lifting for Scientific Computing: A Case Study on FFT
summary
A stepwise semantics lifting approach uses GPT-generated FFT C code and an extended SPIRAL ICode/SigmaSPL pipeline to recover high-level FFT semantics. Symbolic execution produces exact transformation matrices for small n and is used up to n=16 as base cases, then an induction on the recursive matrix relation proves correctness for general n. The prototype performs AST-to-ICode translation, pattern-matches index math to SigmaSPL, and successfully identifies the implementation as a Cooley–Tukey FFT instance.
AI-written summary · about
chapters (9)
- 0:00Semantics lifting intro
- 1:04Why semantics lifting matters
- 2:29FFT verification question
- 4:16Stepwise semantic lifting
- 7:07Reversing SPIRAL generation
- 8:11C to SPIRAL IR for FFT
- 12:25FFT verification results
- 13:30Future work plans
- 14:15Q&A on precision
related talks
11mSemantics Lifting for Scientific Kernels
14mVerification of Algorithm and Code Generation for Signal Transforms- 14mVerification of Algorithm and Code Generation for Signal Transforms
28mFunctional Sparse Tensor Compilation
19mSIMT-Step Execution: A Flexible Operational Semantics For GPU Subgroup Behavior
24mMapping Sparse Applications to Accelerated Computing Systems
19mSpEQ: Translation of Sparse Codes using Equivalences
28mSpEQ: Translation of Sparse Codes using Equivalences