SpEQ: Translation of Sparse Codes using Equivalences

Explore a groundbreaking strategy for detecting semantics in sparse codes and enabling automatic translation to high-performance library calls or domain-specific languages (DSLs) in this 19-minute video presentation from PLDI 2024. Dive into SpEQ, a novel approach that identifies high-level computations along with storage details and related preconditions in sparse linear algebra codes. Learn how SpEQ implements run-time checks to ensure required preconditions are met, guaranteeing correct translations. Discover the implementation details using the LLVM framework, Z3 solver, and egglog library, and see how SpEQ translates sparse linear algebra codes into NVIDIA cuSPARSE, Intel MKL, and OpenMP. Examine the evaluation results across ten diverse benchmarks, showcasing impressive speedups compared to state-of-the-art translation tools. Gain insights into program analysis, verification, equivalence checking, and equality saturation techniques that make SpEQ the only tool capable of guaranteeing correct translation of sparse computations.