SpEQ: Translation of Sparse Codes using Equivalences
summary
SpEQ detects implicit sparse storage, symbolically reconstructs a dense semantics, and uses an equivalence check plus lightweight runtime guards to guarantee correctness before replacing code with library calls. Implementation uses LLVM, Z3, egglog to match CSR-like graphs, generate rewrite rules via equality saturation, and emit cuSPARSE, Intel MKL, or OpenMP calls. Evaluated on ten benchmarks and it produces consistent speedups (geometric means 3.25×, 5.09×, 8.04× for OMP, MKL, cuSPARSE) while proving translations correct.
AI-written summary · about
chapters (12)
- 0:00SpEQ introduction
- 2:07Sparse code translation challenges
- 3:51SpEQ pipeline overview
- 4:34Detecting sparse structures
- 6:20Correctness in sparsity detection
- 7:47Equivalence checking
- 11:18Naming computations
- 13:04Format-free code in EaPo
- 14:33Translation to optimized libraries
- 14:56SpEQ evaluation
- 16:01Tool availability
- 16:21Q&A
related talks
28mFunctional Sparse Tensor Compilation
17mSparseZETA: Intelligent Auto-tuner for Designing High-Performance SpMV Programs
19mGeneralSparse: Bridging the Gap in SpMM for Pruned Large Language Model Inference..
19mCompiler Support for Sparse Tensor Convolutions
15mCompiling and Compressing Structured Tensors
20mVectorizing Sparse Coiteration for Two-finger Loop Structure (Extended Abstract)
13mMind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
15mCompilation of Sparse Array Programming Models