We present S p EQ, a quick and correct strategy for detecting semantics in sparse codes and enabling automatic translation to high-performance library calls or domain-specific languages (DSLs). When sparse linear algebra codes contain implicit preconditions about how data is stored that hamper direct translation, S p EQ identifies the high-level computation along with storage details and related preconditions. A run-time check guards the translation and ensures that required preconditions are met. We implement S p EQ using the LLVM framework, the Z3 solver, and egglog library and correctly translate sparse linear algebra codes into two high-performance libraries, NVIDIA cuSPARSE and Intel MKL, and OpenMP (OMP). We evaluate S p EQ on ten diverse benchmarks against two state-of-the-art translation tools. S p EQ achieves geometric mean speedups of 3.25 × , 5.09 × , and 8.04 × on OpenMP, MKL, and cuSPARSE backends, respectively. S p EQ is the only tool that can guarantee the correct translation of sparse computations.

@article{paperbot2516,
  title = {SpEQ: Translation of Sparse Codes using Equivalences},
  author = {Avery Laird and Bangtian Liu and Nikolaj Bjørner and Maryam Mehri Dehnavi},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {8},
  number = {PLDI},
  year = {2024},
  doi = {10.1145/3656445}
}