CS Compiler Seminar: Damitha Lenadora, "GALA: A High Performance Graph Neural Network Acceleration Language and Compiler," and Heng Zhong, "First-Class Verification Dialects for MLIR."

Event Type

Seminar/Symposium

Sponsor

CS 591 ACT

Location

3102 Siebel Center

Virtual

Join online

Date

Sep 25, 2025   4:00 - 5:00 pm  

Speaker

Damitha Lenadora and Heng Zhong

Contact

Allison Mette

E-Mail

agk@Illinois

Phone

217-300-0256

Originating Calendar

Siebel School Speakers Calendar

Title: GALA: A High Performance Graph Neural Network Acceleration LAnguage and Compiler

Speaker: Damitha Lenadora

Conference: OOPSLA 2025

Author(s): Damitha Lenadora, Nikhil Jayakumar, Chamika Sudusinghe, Charith Mendis

Abstract: Multiple frameworks and optimizations have been proposed for accelerating Graph Neural Network (GNN) workloads over the years, achieving sizable runtime performance improvements. However, we notice that existing systems usually explore optimizing either at the intra-operator level or at the inter-operator level, missing synergies that exist due to their compositions. Further, most existing works focus primarily on optimizing the forward computation of GNNs, often overlooking opportunities for training-specific optimizations.

To exploit these missed optimization opportunities, we introduce GALA, a domain-specific language (DSL) and a compiler that allows composing optimizations at different levels. The GALA DSL exposes intra-operator transformations as scheduling commands, while we introduce novel inter-operator transformations as part of the compiler. The composition of these transformations is made possible through the introduction of two novel intermediate representations (IR) in the GALA compiler that tracks and composes transformations at both the intra- and inter-operator levels. Further, the IRs maintain a global view of the GNN program, including its training process. This allows us to introduce training-specific transformations to aggressively optimize GNN training. Our evaluations show that GALA achieves a geo-mean speedup of 2.55× for inference and 2.52× for training across multiple systems, graphs, and GNN models. We also show that GALA performs well across different graph sizes and GNN model configurations, as well as allows users to explore different methods of performing similar optimizations leading to different tradeoff spaces.

_______________________________________________________________________________________________

Title: First-Class Verification Dialects for MLIR

Speaker: Heng Zhong

Conference: PLDI 2025

Author(s): Mathieu Fehr, Yuyou Fan, Hugo Pompougnac, John Regehr, Tobias Grosser

Abstract: MLIR is a toolkit supporting the development of extensible and composable intermediate representations (IRs) called dialects; it was created in response to rapid changes in hardware platforms, programming languages, and application domains such as machine learning. MLIR supports development teams creating compilers and compiler-adjacent tools by factoring out common infrastructure such as parsers and printers. A major limitation of MLIR is that it is syntax-focused: it has no support for directly encoding the semantics of operations in its dialects. Thus, at present, the parts of MLIR tools that depend on semantics—optimizers, analyzers, verifiers, transformers—must all be engineered by hand.

Our work makes formal semantics a first-class citizen in the MLIR ecosystem. We designed and implemented a collection of semantics-supporting MLIR dialects for encoding the semantics of compiler IRs. These dialects support a separation of concerns between three domains of expertise when building formal-methods-based tooling for compilers. First, compiler developers define their dialect’s semantics as a lowering (compilation transformation) from their dialect to one or more of ours. Second, SMT solver experts provide tools to optimize domain-specific high-level semantics and lower them to SMT queries. Third, tool builders create dialect-independent verification tools.

We validate our work by defining semantics for five key MLIR dialects, defining a state-of-the-art SMT encoding for memory-based semantics, and building three dialect-agnostic tools, which we used to find five miscompilation bugs in upstream MLIR, verify a canonicalization pass, and also formally verify transfer functions for two dataflow analyses: “known bits” (that finds individual bits that are always zero or one in all executions) and “demanded bits” (that finds don’t-care bits). The transfer functions that we verify are improved versions of those in upstream MLIR; they detect on average 36.6% more known bits in real-world MLIR programs compared to the upstream implementation.

Note: The above talk is a student presentation and not by the author(s) of the paper being presented.