SpEQ: Translation of Sparse Codes using Equivalences
summary
SpEQ is a tool (PLDI 2024) that detects when code matches small reference C implementations by translating LLVM IR into e-graphs, adding memory-version returns for stores, and applying rewrite-rule libraries; it uses LLVM, Z3, and egglog and maps matched snippets to OpenMP, Intel MKL or NVIDIA cuSPARSE calls. Evaluated on ten benchmarks, it achieves geometric-mean speedups of 3.25×/5.09×/8.04× (OpenMP/MKL/cuSPARSE) and guarantees correct translation of sparse computations.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 1:04Goal: translating sparse codes
- 2:29SpEQ pipeline overview
- 4:15SpEQ on LLVM IR
- 8:31Memory ops and SSA in LLVM
- 11:05Matching input to reference
- 13:42Flexible rewrite rules
- 15:28Rewrite rules from references
- 16:52Terms for input and reference
- 19:23Overlapping references and cost models
- 20:28Non-sparse vs sparse translation
- 21:10Performance results and detection
- 23:16Extending SpEQ with new references
- 24:20Q&A
related talks
13mSpoq: Scaling Machine-Checkable Systems Verification in Coq
19mOptimizing Ancilla-Based Quantum Circuits with SPARE
14mVerification of Algorithm and Code Generation for Signal Transforms
28mFunctional Sparse Tensor Compilation- 14mVerification of Algorithm and Code Generation for Signal Transforms
23mModular Construction and Optimization of the UZP Sparse Format for SpMV on CPUs
11mQiMeng-Xpiler: Transcompiling Tensor Programs for Deep Learning Systems with a...
20mExploiting Sparsity and Redundancy