SpEQ: Translation of Sparse Codes using Equivalences
Open Access
- 20 June 2024
- journal article
- abstracts
- Published by Association for Computing Machinery (ACM) in Proceedings of the ACM on Programming Languages
- Vol. 8 (PLDI) , 1680-1703
Abstract
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.Keywords
Funding Information
- NSERC (RGPIN-06516, DGECR00303)
This publication has 43 references indexed in Scilit:
- An Approach for Proving the Correctness of Inspector/Executor Transformations2015
- Witnessing Program Transformations2013
- Introduction to Bisimulation and Coinduction2011
- Equality saturationACM SIGPLAN Notices, 2009
- Z3: An Efficient SMT Solver2008
- Efficient E-Matching for SMT Solvers2007
- Direct Methods for Sparse Linear Systems2006
- Simplify: a theorem prover for program checkingJournal of the ACM, 2005
- Temporal Verification of Reactive Systems1995
- Automatic generation of invariants and intermediate assertions1995