2/13/2025 Hannah Gainer
CS professor Charith Mendis and CS second-year PhD student, Jai Arora, won the Distinguished Paper Award at Principles of Programming Languages (POPL) 2025. The paper submission that won them the Distinguished Paper Award concerned verifying the correctness of tensor compilers.
Written by Hannah Gainer
CS professor Charith Mendis and CS second-year PhD student, Jai Arora, won the Distinguished Paper Award at Principles of Programming Languages (POPL) 2025.
The paper submission that won them the Distinguished Paper Award concerned verifying the correctness of tensor compilers. “This paper presents a methodology to automatically verify tensor graph rewrites, a compiler optimization, present in tensor compilers such as XLA. Tensor compilers form the backbone of modern deep learning workloads, and this work builds confidence into their correctness,” said Mendis.
Arora led the project. "Jai’s knowledge of compilers and formal methods is commendable and the project was a great fit for him. From the beginning, we wanted to work with our industry partners to make the project impactful," Mendis said. He added that Arora worked in, "close collaboration with XLA compiler team at Google and collaborators from Google DeepMind, the University of Washington, and the University of California Santa Cruz."
“Before joining U. of I. as a Ph.D. Student, I was interested in working on a project at the intersection of Compilers and Formal Methods,” said Arora. “Fortunately, I found a great fit in Professor Charith's research group and started to work on this project. It was great to work with awesome researchers and industry partners!”
The collaborators included Devansh Jain, Tianfan Xu, Farzin Houshmand, Phitchaya Mangpo Phothilimthana, Praveen Narayanan, Karthik Srinivasa Murthy, Rastislav Bodik, Amit Sabne, Sirui Lu, and Mohsen Lesani.
Mendis shared that this project started after noticing that there isn’t much work done for emerging compilation platforms such as tensor compilers which are the backbone for neural network workloads compared to general-purpose compilers such as LLVM.
Mendis said, “It is important to build confidence that these compilers are doing the right thing and this observation prompted us to start this project. As the Turing Award lecture from Ken Thompson mentions, we need to be able to trust the trust and it is paramount in the case of tensor compilers that power the AI revolution!”
“Further, we wanted explicitly to target a production-quality tensor compiler that is used by many ML practitioners even though we knew formalizing its components would be challenging,” Mendis said.
POPL serves as a forum discussing all aspects of programming languages and systems. Both theoretical and experimental papers are welcome, covering topics from formal frameworks to experience reports. Submissions should make principled, lasting contributions to the theory, design, understanding, implementation, or application of programming languages.
The Review Committee will evaluate the technical contribution of each submission and its accessibility to experts and the POPL audience. Each paper must explain its scientific contribution in general and technical terms, identifying what has been accomplished, its significance, and how it compares to previous work.
Mendis said, “The Distinguished Paper Award at POPL is only awarded to at most 10% of the accepted papers, which rewards papers for their originality, relevance, significance, and clarity. It is a significant distinction, and it feels great that our work was recognized for the same.” POPL 2025 employed a full double-blind reviewing process, as in previous years.
This paper will inspire other projects. Mendis is looking to extend this project to handle a class of tensor graph rewrites that aren’t currently supported. Supporting these extensions would bring them closer to provably correct tensor compilers.
Grainger Engineering Affiliations
Charith Mendis is an Illinois Grainger Engineering professor of computer science.