一句话：SpEQ 识别稀疏代码语义与存储前置条件，并将其正确翻译为高性能库或 DSL 调用。
稀疏线性代数代码常隐含数据存储前置条件，直接翻译到高性能库或 DSL 容易产生错误。SpEQ 通过等价关系识别高层计算、存储细节及相关前置条件，并用运行时检查守护翻译，确保所需条件满足。其实现基于 LLVM、Z3 与 egglog，可将稀疏代码正确翻译到 NVIDIA cuSPARSE、Intel MKL 和 OpenMP。在十个多样基准上对比两个先进翻译工具，SpEQ 在 OMP、MKL、cuSPARSE 后端分别取得 3.25×、5.09×、8.04× 的几何平均加速，并且是唯一能保证稀疏计算正确翻译的工具。
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}
}