Search Results

Documents authored by Cheung, Alvin

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}
}
Document
Experience Paper
DOI: 10.4230/LIPIcs.ECOOP.2023.38
Building Code Transpilers for Domain-Specific Languages Using Program Synthesis (Experience Paper)

Authors: Sahil Bhatia, Sumer Kohli, Sanjit A. Seshia, and Alvin Cheung

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
Domain-specific languages (DSLs) are prevalent across many application domains. Such languages let developers easily express computations using high-level abstractions that result in performant implementations. To leverage DSLs, however, application developers need to master the DSL’s syntax and manually rewrite existing code. Compilers can aid in this effort, but part of building a compiler requires transpiling code from the source code to the target DSL. Such transpilation is typically done via pattern-matching rules on the source code. Sadly, developing such rules is often a painstaking and error-prone process. In this paper, we describe our experience in using program synthesis to build code transpilers. To do so, we developed MetaLift, a new framework for building transpilers that transform general-purpose code into DSLs using program synthesis. To use MetaLift, transpiler developers first define the target DSL’s semantics using MetaLift’s specification language, and specify the search space for each input code fragment to be transpiled using MetaLift’s API. MetaLift then leverages program synthesizers and theorem provers to automatically find transpilations expressed in the target DSL that is provably semantic equivalent to the input code. We have used MetaLift to build three DSL transpilers targeting different programming models and application domains. Our results show that the MetaLift-based compilers can translate many benchmarks used in prior work created by specialized implementations, but can be built using orders-of-magnitude fewer lines of code as compared to prior work.
Cite as

Sahil Bhatia, Sumer Kohli, Sanjit A. Seshia, and Alvin Cheung. Building Code Transpilers for Domain-Specific Languages Using Program Synthesis (Experience Paper). In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 38:1-38:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bhatia_et_al:LIPIcs.ECOOP.2023.38,
  author =	{Bhatia, Sahil and Kohli, Sumer and Seshia, Sanjit A. and Cheung, Alvin},
  title =	{{Building Code Transpilers for Domain-Specific Languages Using Program Synthesis}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{38:1--38:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim 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.2023.38},
  URN =		{urn:nbn:de:0030-drops-182316},
  doi =		{10.4230/LIPIcs.ECOOP.2023.38},
  annote =	{Keywords: Program Synthesis, Code Transpilation, DSLs, Verification}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2015.51
Bridging the Gap Between General-Purpose and Domain-Specific Compilers with Synthesis

Authors: Alvin Cheung, Shoaib Kamil, and Armando Solar-Lezama

Published in: LIPIcs, Volume 32, 1st Summit on Advances in Programming Languages (SNAPL 2015)

Abstract
This paper describes a new approach to program optimization that allows general purpose code to benefit from the optimization power of domain-specific compilers. The key to this approach is a synthesis-based technique to raise the level of abstraction of general-purpose code to enable aggressive domain-specific optimizations. We have been implementing this approach in an extensible system called Herd. The system is designed around a collection of parameterized kernel translators. Each kernel translator is associated with a domain-specific compiler, and the role of each kernel translator is to scan the input code in search of code fragments that can be optimized by the domain-specific compiler embedded within each kernel translator. By leveraging general synthesis technology, it is possible to have a generic kernel translator that can be specialized by compiler developers for each domain-specific compiler, making it easy to build new domain knowledge into the overall system. We illustrate this new approach to build optimizing compilers in two different domains, and highlight research challenges that need to be addressed in order to achieve the ultimate vision.
Cite as

Alvin Cheung, Shoaib Kamil, and Armando Solar-Lezama. Bridging the Gap Between General-Purpose and Domain-Specific Compilers with Synthesis. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 51-62, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{cheung_et_al:LIPIcs.SNAPL.2015.51,
  author =	{Cheung, Alvin and Kamil, Shoaib and Solar-Lezama, Armando},
  title =	{{Bridging the Gap Between General-Purpose and Domain-Specific Compilers with Synthesis}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{51--62},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-80-4},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{32},
  editor =	{Ball, Thomas and Bodík, Rastislav and Krishnamurthi, Shriram and Lerner, Benjamin S. and Morriset, Greg},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2015.51},
  URN =		{urn:nbn:de:0030-drops-50162},
  doi =		{10.4230/LIPIcs.SNAPL.2015.51},
  annote =	{Keywords: compilers, domain-specific languages, program synthesis, cross compilation, 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