Verified Tensor-Program Optimization Via High-Level Scheduling Rewrites
summary
A Coq-verified framework implements a pure functional tensor IR called ATL and a suite of semantics-preserving, source-to-source rewrites plus reshape operators to decouple compute order from storage; tactics automate the proof obligations and lower to C via trusted compilation. Benchmarks show schedule choice causes up to a 40x speedup (and simple bad swaps give ~2x slowdown), the system matches Halide-class performance, expresses tiling, transposes, and converts batched convolutions into matrix–matrix multiplies; artifacts and evaluated reproducible runs are available.
AI-written summary · about
chapters (17)
- 0:00Intro
- 0:24High-Performance Computing Domains
- 1:08Algorithms v. Schedules: Blur
- 1:58Scheduling Loops: Fusion
- 2:24Scheduling Loops: Tiles
- 3:23Scheduling Massively Affects Performance
- 4:26Scheduling Through Rewrites
- 6:10Goals
- 7:50Core ATL Constructs and Their Lowering
- 9:46A Simple Scatter in ATL
- 10:32Rewriting Using Theorems
- 11:50Proof-generating Scheduling Scripts
- 14:54Imperative Control to Decouple Compute and Storage
- 16:18Reshape Operator Adjoints
- 16:42Introducing Reshape Operators Using Adjoint Rewrites
- 18:56Expressivity for Competitive Performance
- 19:23Expressivity Beyond Halide
related talks
18mA Verified Compiler for a Functional Tensor Language
20mA Mechanized Algebra of Verified Data Structures for Optimizing Sparse Tensor Programs
28mFunctional Sparse Tensor Compilation
33mTeIL: a type-safe imperative Tensor Intermediate Language
19mCompiler Support for Sparse Tensor Convolutions
14mAchieving High-Performance the Functional Way - A Functional Pearl on Expressing High...
11mQiMeng-Xpiler: Transcompiling Tensor Programs for Deep Learning Systems with a...
15mCertified and Efficient Instruction Scheduling: Application to Interlocked VLIW Processors