Indexed Streams: A Formal Intermediate Representation for the Fused Execution of Contraction Operations

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.

Article

Movie

BibTeX

@article{kovach2023,
  title={Indexed Streams: A Formal Intermediate Representation for the Fused Execution of Contraction Operations},
  author={Scott Kovach and Praneeth Kolichala and Timothy Gu and Fredrik Kjolstad},
  journal={Proceedings of the ACM on Programming Languages},
  volume={7},
  issue={PLDI},
  year={2023},
  month={June}
}