paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Indexed Streams: A Formal Intermediate Representation for Fused Contraction Programs

索引流:融合收缩程序的形式化中间表示
PLDI 7(PLDI)2023匹配度 4/10 · 论文属于PL/编译器方向,涉及稀疏张量与关系代数融合执行的形式化IR,有形式语义和正确性证明,与机器学习系统编译有一定关联;但不涉及用户核心关注的静态分析、Agentic程序、LLM、浮点程序分析或贝叶斯程序分析,方向匹配度有限。引用 11 inbox
Scott Kovach, Praneeth Kolichala, Tiancheng Gu, Fredrik Kjolstad
crossref: 2026-09-10

AI 速览

一句话:提出索引流:统一稀疏张量与关系代数融合收缩执行的形式化中间表示,证明正确性且性能可比专用系统。

论文针对稀疏张量代数与关系代数中普遍存在的收缩(contraction)与融合执行,缺乏统一形式化中间表示的问题,提出索引流(indexed streams)。索引流是一种形式化操作模型和中间表示,用于描述收缩语言的融合执行,可同时覆盖稀疏张量代数与关系代数。作者证明该模型相对于函数式语义是正确的,并基于索引流实现了一个收缩表达式编译器。该编译器仅 540 行代码,但实验表明其性能可分别匹配面向稀疏张量代数的 TACO 编译器,以及面向关系代数的 SQLite 与 DuckDB 查询处理库。这展示了统一 IR 在跨领域融合计算中的可行性与效率。

问题
如何用统一的形式化中间表示描述稀疏张量代数与关系代数中收缩表达式的融合执行,并同时保证语义正确性与高性能。
方法
提出索引流这一形式化操作模型与中间表示,证明其相对函数式语义的正确性,并实现一个仅 540 行的收缩表达式编译器。
评估
将基于索引流的编译器与稀疏张量代数编译器 TACO、关系代数查询处理库 SQLite 和 DuckDB 进行性能对比,表明其可匹配这些专用系统。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@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}
}