SpEQ: Translation of Sparse Codes using Equivalences
summary
SpEQ detects sparse-data semantics via equivalence checks that prove a CSR-style loop is equivalent to a dense reference, then uses e-graphs (equality saturation) to match and rewrite into known kernels. Implemented with LLVM, Z3, and egglog (Python glue), it translates to OpenMP, Intel MKL and cuSPARSE and runs on ten benchmarks, giving geometric mean speedups of 3.25×, 5.09× and 8.04× while claiming the only guarantee of correct translation and modest latency close to O3.
AI-written summary · about
chapters (11)
- 0:00SpEQ introduction
- 1:06Motivation for translation
- 3:53SpEQ pipeline overview
- 5:37Detecting storage formats
- 8:07Equivalence checking
- 10:17Proving equivalence
- 12:27Transition systems formalization
- 14:17Semantics via equality saturation
- 16:06SpEQ evaluation
- 17:11Using SpEQ artifacts
- 17:55Q&A
related talks
28mFunctional Sparse Tensor Compilation
20mExploiting Sparsity and Redundancy
14mVerification of Algorithm and Code Generation for Signal Transforms- 14mVerification of Algorithm and Code Generation for Signal Transforms
13mSpoq: Scaling Machine-Checkable Systems Verification in Coq
13mMind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
30megg: Fast and Extensible Equality Saturation
11mSemantics Lifting for Scientific Kernels