一句话:提出索引流:统一稀疏张量与关系代数融合收缩执行的形式化中间表示,证明正确性且性能可比专用系统。
论文针对稀疏张量代数与关系代数中普遍存在的收缩(contraction)与融合执行,缺乏统一形式化中间表示的问题,提出索引流(indexed streams)。索引流是一种形式化操作模型和中间表示,用于描述收缩语言的融合执行,可同时覆盖稀疏张量代数与关系代数。作者证明该模型相对于函数式语义是正确的,并基于索引流实现了一个收缩表达式编译器。该编译器仅 540 行代码,但实验表明其性能可分别匹配面向稀疏张量代数的 TACO 编译器,以及面向关系代数的 SQLite 与 DuckDB 查询处理库。这展示了统一 IR 在跨领域融合计算中的可行性与效率。
We introduce indexed streams, a formal operational model and intermediate representation that describes the fused execution of a contraction language that encompasses both sparse tensor algebra and relational algebra. We prove that the indexed stream model is correct with respect to a functional semantics. We also develop a compiler for contraction expressions that uses indexed streams as an intermediate representation. The compiler is only 540 lines of code, but we show that its performance can match both the TACO compiler for sparse tensor algebra and the SQLite and DuckDB query processing libraries for relational algebra.
@article{paperbot1991,
title = {Indexed Streams: A Formal Intermediate Representation for Fused Contraction Programs},
author = {Scott Kovach and Praneeth Kolichala and Tiancheng Gu and Fredrik Kjolstad},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591268}
}