Talks¶
We regularly present our work at the LLVM Developer Meetings: here are the talks of our team and our interns, from the first presentation of Polly in 2010 to today. Click a thumbnail to watch.
2026

Scaling Certified Instruction Selection For LLVM IR Through Bitblasting
Sarah Linh Kuhn, Luisa Cicolini
An LLVM instruction selector verified in Lean: using Sail's Lean backend for authoritative RISC-V semantics, we automatically verify real LLVM instruction selection and optimization patterns.

Toward A More Declarative InstCombine: Generalization & Parametric Bitvector Algorithms
New parametric bitvector algorithms lift InstCombine's fixed-width tests into width-independent identities, moving LLVM toward a declarative, provably correct InstCombine.
Tamagoyaki: MLIR-Native Equality Saturation
Sasha Lopoukhine, Jules Merckx, Sam Coward, Jianyi Cheng, Bjorn De Sutter, Tobias Grosser
A framework that represents equivalences directly in MLIR and xDSL IR, bringing equality saturation to existing rewrite patterns, demonstrated by replicating the core of Herbie.
Non-destructive PDL Rewriting for Multi-Level Equality Saturation
Jules Merckx, Sasha Lopoukhine
E-graphs as MLIR IR: new PDL operations for non-destructive rewriting make equality saturation available at every level of abstraction.
2025

Specializing MLIR Data Structures: an Experiment
What happens when we specialize MLIR's core data structures for a single dialect? Challenges, solutions, and lessons for faster MLIR compilers.

Automatically generating pattern rewrites in MLIR
Instead of writing rewrite rules by hand, we generate MLIR pattern rewrites automatically from a high-level specification.

How to trust your peephole rewrites: automatically verifying them for arbitrary width!
Algorithms, implemented and proven correct in Lean, that verify peephole rewrites for all bitwidths at once, applied to Hacker's Delight and InstCombine.

Dialects as a Dialect: Bringing native C++ registration to IRDL
A new tool generates C++ definitions from IRDL, so declaratively defined dialects work with C++ patterns and dialect conversion, just like ODS.
2024

Unlocking High Performance in Mojo through User-Defined Dialects
Mathieu Fehr, Jeff Niu
Mojo merges libraries and embedded DSLs by letting users extend its MLIR-based compiler with their own dialects.

Quidditch: An End-to-End Deep Learning Compiler for Occamy using IREE & xDSL
Markus Böck, Sasha Lopoukhine
From a neural network description to fast code on ETH's chiplet-based Occamy accelerator, combining IREE with a RISC-V micro-kernel compiler in xDSL.

DynamicAPInt: Infinite-Precision Arithmetic for LLVM
A new LLVM class for arbitrary-precision integers, with a small-value optimization that makes it up to 2.8x faster than APInt.

Exploiting MLIR Abstractions for Hardware Verification
Generating verification models from CIRCT's high-level finite state machine dialect, to check hardware properties where they are easiest to state.

Is MLIR feature complete? Production ready?
Alex Zinenko, Stella Laurenzo, Renato Golin, Tobias Grosser, Mehdi Amini, Chris Lattner
A panel on where MLIR stands as upstream development slows down and more work moves to downstream projects.

lean-mlir: A Workbench for formally verifying Peephole Optimizations for MLIR
An Alive-style workflow in Lean: define peephole rewrites over LLVM-style IRs and verify them with proof automation.
xdsl-gui: A Playground for the Compiler Optimization Game
An interactive environment to apply compiler passes step by step, watch the IR change, and get real-time feedback on which passes apply.
accfg: Eliminating Setup Overhead for Accelerator Dispatch
Anton Lydike, Josse Van Delm
A compiler dialect that removes redundant accelerator configuration, with significant speed-ups on three accelerator platforms.

Arcilator for ages five and up: flexible self-contained hardware simulation made easy
A dialect-based interface for the CIRCT hardware simulator Arcilator that removes the need for hand-written C++ wrappers.

Teaching MLIR concepts to undergraduate students
Mathieu Fehr, Sasha Lopoukhine
An undergraduate compiler course at Edinburgh, with every step from parsing to RISC-V assembly expressed in MLIR.
2023

An MLIR Backend for Linear Algebra
A RISC-V backend dialect in MLIR that keeps high-level information during lowering, models hardware extensions as dialects, and allocates registers in SSA form.

MPI Dialect For MLIR
Bringing MPI into MLIR as a dialect, enabling automatic domain decomposition entirely within MLIR.

Arcilator: Fast And Cycle Accurate Hardware Simulation In CIRCT
Martin Erhart
A cycle-accurate hardware simulator in CIRCT that compiles designs straight to LLVM IR, with performance comparable to Verilator.

Extending Dominance To MLIR Regions
Siddharth Bhat, Jeff Niu
Where LLVM's notion of dominance breaks down in MLIR's regions, and possible ways forward.

MLIR Side Effect Modeling
Siddharth Bhat, Jeff Niu
A review of MLIR's memory effect interfaces, their limits for undefined behaviour and parallelism, and proposals to evolve them.

mlir-meminfo: A Memory Model for MLIR
Kunwar Grover, Arjun Pitchanathan
A lightweight analytical model that predicts the cache behaviour of MLIR programs and composes across transformations.

mlirSynth: Synthesis of Domain-Specific Programs in MLIR
Alexander Brauckmann
Automatically raising programs to high-level MLIR dialects by program synthesis from dialect definitions, instead of hand-written rules.

Fast pivot Function for MLIR's Presburger Library Through Vectorization and Integer Arithmetic in FPU
Qi Zhou
Speeding up the core of MLIR's Presburger library with vectorized, overflow-checked integer arithmetic on the FPU.

Prototyping MLIR in Python
Sasha Lopoukhine, Mathieu Fehr
xDSL, a pure-Python reimplementation of MLIR's core that lowers the barrier to entry and speeds up prototyping of dialects.
2022

IRDL: A Dialect for dialects
A dialect for defining dialects declaratively, registered dynamically at runtime, with optimized verifiers.

MLIR for Functional Programming
An MLIR-based backend for the Lean 4 theorem prover, and what MLIR needs to support functional languages well.

Precise Polyhedral Analyses For MLIR using the FPL Presburger Library
A tutorial on MLIR's Presburger library: precise reasoning about integer sets for cache models, loop optimization, and verification.

Finding Missed Optimizations Through the Lens of Dead Code Elimination
Using dead code elimination as a lens to automatically find missed optimizations in GCC and LLVM.
2017

Scale, Robust and Regression-Free Loop Optimizations for Scientific Fortran and Modern C++
Tobias Grosser, Michael Kruse
How Polly became a scalable, robust, and regression-free loop optimizer for modern C++ and large scientific codes.

Enabling Polyhedral optimizations in TensorFlow through Polly
Annanay Agarwal, Michael Kruse, Brian Retford, Tobias Grosser, Ramakrishna Upadrasta
Speeding up deep learning kernels such as convolutions with Polly's polyhedral loop transformations.
2016

Enabling Polyhedral Optimizations in Julia
Matthias Reisinger
Bringing Polly's loop optimizations to the Julia language.

How Polyhedral Modeling enables compilation to Heterogeneous Hardware
Tobias Grosser
Using Polly's precise memory footprints and access remapping to compile for accelerators, up to automatic PTX/CUDA code generation.

Analyzing and Optimizing your Loops with Polly
Tobias Grosser, Johannes Doerfert
A hands-on tutorial: did Polly understand my loops, what did it learn about them, and how can it make them faster?
2015

Tutorial: Polly - Optimistic Loop Nest Optimizations with Schedule Trees
Tobias Grosser, Johannes Doerfert
Modeling loop programs with integer-set schedule trees, and how Polly uses optimistic assumptions to optimize real-world loop nests.
2011

Polly - First successful optimizations - How to proceed?
Tobias Grosser
One year in: Polly loads into clang -O3, generates SIMD and OpenMP code, and shows its first significant speed-ups over clang.
