Search Results

Documents authored by Cai, Colin

Document
DOI: 10.4230/LIPIcs.ECOOP.2024.32
Tenspiler: A Verified-Lifting-Based Compiler for Tensor Operations

Authors: Jie Qiu, Colin Cai, Sahil Bhatia, Niranjan Hasabnis, Sanjit A. Seshia, and Alvin Cheung

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
Tensor processing infrastructures such as deep learning frameworks and specialized hardware accelerators have revolutionized how computationally intensive code from domains such as deep learning and image processing is executed and optimized. These infrastructures provide powerful and expressive abstractions while ensuring high performance. However, to utilize them, code must be written specifically using the APIs / ISAs of such software frameworks or hardware accelerators. Importantly, given the fast pace of innovation in these domains, code written today quickly becomes legacy as new frameworks and accelerators are developed, and migrating such legacy code manually is a considerable effort. To enable developers in leveraging such DSLs while preserving their current programming paradigm, we present Tenspiler, a verified-lifting-based compiler that uses program synthesis to translate sequential programs written in general-purpose programming languages (e.g., C++ or Python code that does not leverage any specialized framework or accelerator) into tensor operations. Central to Tenspiler is our carefully crafted yet simple intermediate language, named TensIR, that expresses tensor operations. TensIR enables efficient lifting, verification, and code generation. Unlike classical pattern-matching-based compilers, Tenspiler uses program synthesis to translate input code into TensIR, which is then compiled to the target API / ISA. Currently, Tenspiler already supports six DSLs, spanning a broad spectrum of software and hardware environments. Furthermore, we show that new backends can be easily supported by Tenspiler by adding simple pattern-matching rules for TensIR. Using 10 real-world code benchmark suites, our experimental evaluation shows that by translating code to be executed on 6 different software frameworks and hardware devices, Tenspiler offers on average 105× kernel and 9.65× end-to-end execution time improvement over the fully-optimized sequential implementation of the same benchmarks.
Cite as

Jie Qiu, Colin Cai, Sahil Bhatia, Niranjan Hasabnis, Sanjit A. Seshia, and Alvin Cheung. Tenspiler: A Verified-Lifting-Based Compiler for Tensor Operations. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 32:1-32:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{qiu_et_al:LIPIcs.ECOOP.2024.32,
  author =	{Qiu, Jie and Cai, Colin and Bhatia, Sahil and Hasabnis, Niranjan and Seshia, Sanjit A. and Cheung, Alvin},
  title =	{{Tenspiler: A Verified-Lifting-Based Compiler for Tensor Operations}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{32:1--32:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.32},
  URN =		{urn:nbn:de:0030-drops-208817},
  doi =		{10.4230/LIPIcs.ECOOP.2024.32},
  annote =	{Keywords: Program Synthesis, Code Transpilation, Tensor DSLs, Verification}
}
Document
Artifact
DOI: 10.4230/DARTS.10.2.17
Tenspiler: A Verified-Lifting-Based Compiler for Tensor Operations (Artifact)

Authors: Jie Qiu, Colin Cai, Sahil Bhatia, Niranjan Hasabnis, Sanjit A. Seshia, and Alvin Cheung

Published in: DARTS, Volume 10, Issue 2, Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
In the related article, we described Tenspiler, a verified-lifting-based compiler that translates sequential programs to tensor operations. We further demonstrated its effectiveness by translating 69 benchmarks from into 6 different DSL targets and evaluating their performance against the baseline. This artifact includes the implementation of Tenspiler as well as files used to reproduce those results.
Cite as

Jie Qiu, Colin Cai, Sahil Bhatia, Niranjan Hasabnis, Sanjit A. Seshia, and Alvin Cheung. Tenspiler: A Verified-Lifting-Based Compiler for Tensor Operations (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 17:1-17:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{qiu_et_al:DARTS.10.2.17,
  author =	{Qiu, Jie and Cai, Colin and Bhatia, Sahil and Hasabnis, Niranjan and Seshia, Sanjit A. and Cheung, Alvin},
  title =	{{Tenspiler: A Verified-Lifting-Based Compiler for Tensor Operations (Artifact)}},
  pages =	{17:1--17:2},
  journal =	{Dagstuhl Artifacts Series},
  ISBN =	{978-3-95977-342-3},
  ISSN =	{2509-8195},
  year =	{2024},
  volume =	{10},
  number =	{2},
  editor =	{Qiu, Jie and Cai, Colin and Bhatia, Sahil and Hasabnis, Niranjan and Seshia, Sanjit A. and Cheung, Alvin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.17},
  URN =		{urn:nbn:de:0030-drops-209150},
  doi =		{10.4230/DARTS.10.2.17},
  annote =	{Keywords: Program Synthesis, Code Transpilation, Tensor DSLs, Verification}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact