Publications

2025

1. arXiv

   ACT: Automatically Generating Compiler Backends from Tensor Accelerator ISA Descriptions

   Devansh Jain, Akash Pardeshi, Marco Frigo, Krut Patel, Kaustubh Khulbe, Jai Arora, and Charith Mendis

   Oct 2025

   Abs DOI Bib PDF

   Tensor compilers play a key role in enabling high-performance implementations of deep learning workloads. These compilers rely on existing CPU and GPU code generation backends to generate device-specific code. Recently, many tensor accelerators (neural processing units) have been proposed to further accelerate these workloads. Compared to commodity hardware, however, most of the proposed tensor accelerators do not have compiler backends with code generation support. Moreover, the accelerator designs are subject to fast iteration cycles, making it difficult to manually develop compiler backends similar to commodity hardware platforms. Therefore, to increase adoption and enable faster software development cycles for novel tensor accelerator designs, we need to make the compiler backend construction process more agile. To address this gap, we introduce ACT, a compiler backend generator that automatically generates compiler backends for tensor accelerators, given just the instruction set architecture (ISA) descriptions. We first formally specify the compiler backend generation problem that introduces a novel specification for describing tensor accelerator ISAs. Next, we design ACT such that it supports user-programmable memories and complex parameterized instructions that are prevalent in tensor accelerators. ACT uses a novel parameterized equality saturation-based instruction selection phase and a constraint programming-based memory allocation phase. We prove that compiler backends generated by ACT are sound and complete. Finally, we generate compiler backends for three accelerator platforms from industry and academia, and show that they match or outperform code written using hand-optimized kernel libraries while maintaining low compilation overheads.

   @article{jain2025actautomaticallygeneratingcompiler,
     title = {ACT: Automatically Generating Compiler Backends from Tensor Accelerator ISA Descriptions},
     author = {Jain, Devansh and Pardeshi, Akash and Frigo, Marco and Patel, Krut and Khulbe, Kaustubh and Arora, Jai and Mendis, Charith},
     year = {2025},
     eprint = {2510.09932},
     archiveprefix = {arXiv},
     primaryclass = {cs.PL},
     url = {https://arxiv.org/abs/2510.09932},
     doi = {10.48550/arXiv.2510.09932},
     month = oct
   }

2. MICRO

   TAIDL: Tensor Accelerator ISA Definition Language with Auto-generation of Scalable Test Oracles

   Devansh Jain, Marco Frigo, Jai Arora, Akash Pardeshi, Zhihao Wang, Krut Patel, and Charith Mendis

   In Proceedings of the 58th IEEE/ACM International Symposium on Microarchitecture (MICRO), Oct 2025

   Abs DOI Bib PDF

   With the increasing importance of deep learning workloads, many hardware accelerators have been proposed in both academia and industry. However, software tooling for the vast majority of them does not exist compared to the software ecosystem and innovations proposed for established platforms such as CPUs and GPUs. We observed that the lack of well-defined hardware-software interfaces and correctness testing tools like fast and scalable test oracles (also known as functional simulators) act as significant barriers to adopting these emerging accelerators in the software community. These interfaces and tools are essential in building software such as retargetable compilers and optimized kernels. To bridge these gaps, we first present TAIDL, an instruction specification language that provides novel constructs to describe the instruction set architectures (ISAs) of tensor accelerators. Next, given ISA definitions in TAIDL, we introduce techniques to automatically generate fast and scalable test oracles for diverse sets of accelerators, which are needed for testing software correctness of code that targets pre-silicon hardware designs. Automated generation of such tools reduces the burden on hardware architects and the repeated development efforts required across different accelerator platforms. Further, our techniques allow us to execute these simulators on GPUs, leading to highly scalable simulations. To demonstrate the expressivity of TAIDL, we instantiated several tensor accelerator ISAs with different compute capabilities and memory hierarchies. Further, we show that test oracles generated using TAIDL definitions are orders of magnitude faster and more scalable than existing instruction-level functional simulators, making them suitable for integration into software development cycles. TAIDL is available at https://github.com/act-compiler/taidl.

   @inproceedings{10.1145/3725843.3756075,
     author = {Jain, Devansh and Frigo, Marco and Arora, Jai and Pardeshi, Akash and Wang, Zhihao and Patel, Krut and Mendis, Charith},
     title = {TAIDL: Tensor Accelerator ISA Definition Language with Auto-generation of Scalable Test Oracles},
     year = {2025},
     isbn = {9798400715730},
     publisher = {Association for Computing Machinery},
     address = {New York, NY, USA},
     url = {https://doi.org/10.1145/3725843.3756075},
     doi = {10.1145/3725843.3756075},
     booktitle = {Proceedings of the 58th IEEE/ACM International Symposium on Microarchitecture (MICRO)},
     month = oct,
     pages = {1316-1333},
     numpages = {18},
     series = {MICRO '25},
   }

3. POPL

   TensorRight: Automated Verification of Tensor Graph Rewrites

   Jai Arora, Sirui Lu, Devansh Jain, Tianfan Xu, Farzin Houshmand, Phitchaya Mangpo Phothilimthana, Mohsen Lesani, Praveen Narayanan, Karthik Srinivasa Murthy, Rastislav Bodik, Amit Sabne, and Charith Mendis

   Proc. ACM Program. Lang. (POPL), Jan 2025

   🏆 Distinguished Paper Award

   Abs DOI arXiv Bib PDF Supp Code

   Tensor compilers, essential for generating efficient code for deep learning models across various applications, employ tensor graph rewrites as one of the key optimizations. These rewrites optimize tensor computational graphs with the expectation of preserving semantics for tensors of arbitrary rank and size. Despite this expectation, to the best of our knowledge, there does not exist a fully automated verification system to prove the soundness of these rewrites for tensors of arbitrary rank and size. Previous works, while successful in verifying rewrites with tensors of concrete rank, do not provide guarantees in the unbounded setting. To fill this gap, we introduce TensorRight, the first automatic verification system that can verify tensor graph rewrites for input tensors of arbitrary rank and size. We introduce a core language, TensorRight DSL, to represent rewrite rules using a novel axis definition, called aggregated-axis, which allows us to reason about an unbounded number of axes. We achieve unbounded verification by proving that there exists a bound on tensor ranks, under which bounded verification of all instances implies the correctness of the rewrite rule in the unbounded setting. We derive an algorithm to compute this rank using the denotational semantics of TensorRight DSL. TensorRight employs this algorithm to generate a finite number of bounded-verification proof obligations, which are then dispatched to an SMT solver using symbolic execution to automatically verify the correctness of the rewrite rules. We evaluate TensorRight’s verification capabilities by implementing rewrite rules present in XLA’s algebraic simplifier. The results demonstrate that TensorRight can prove the correctness of 115 out of 175 rules in their full generality, while the closest automatic, bounded-verification system can express only 18 of these rules.

   @article{10.1145/3704865,
     author = {Arora, Jai and Lu, Sirui and Jain, Devansh and Xu, Tianfan and Houshmand, Farzin and Phothilimthana, Phitchaya Mangpo and Lesani, Mohsen and Narayanan, Praveen and Murthy, Karthik Srinivasa and Bodik, Rastislav and Sabne, Amit and Mendis, Charith},
     title = {TensorRight: Automated Verification of Tensor Graph Rewrites},
     year = {2025},
     issue_date = {January 2025},
     publisher = {Association for Computing Machinery},
     address = {New York, NY, USA},
     volume = {9},
     number = {POPL},
     url = {https://doi.org/10.1145/3704865},
     doi = {10.1145/3704865},
     journal = {Proc. ACM Program. Lang. (POPL)},
     month = jan,
     articleno = {29},
     numpages = {32},
     keywords = {Denotational Semantics, Tensor Compilers, Unbounded Verification},
     note = {<span style="color: red;"><b>🏆 Distinguished Paper Award</b></span>}
   }