Distinguished (for me) Papers of PLDI'25
I had a blast at PLDI'25 this year! The best part, of course, was Marisa's talk about Spineless Traversal, but I wanted to take list the other highlights of the event, both for my own memory and for others who share my research taste. My inspiration is Phil Zucker, whose PLDI post is just phenomenal. I think of the papers below as getting a "Distinguished Paper" award from me.
EGRAPHS'25
This was my first time attending EGRAPHS. Isn't that kind of crazy? It's the fourth edition and it's my first time! Well, somehow I missed the other three; the only time I had a paper at that PLDI was in 2022, when we'd just had a boy and Ian had to give the presentation alone.
Automated High-Level Synthesis Design Modularization via E-Graph Anti-Unification, by A. Wanna C. Hao, and T. Drane was one big highlight for me. This project seems to have put together a huge pipeline, using polymorphic optimization to "normalize" loop nests before doing some e-graph based "matching" to find common codes across multiple programs that could then be synthesized into hardware. I'll definitely be studying this because we're trying to do something similar in Herbie. Also, this use of polyhedral optimization was really inspiring, both because this "normalization" approach is something I haven't seen before and also because it makes me think implementing polyhedral maybe wouldn't be that hard?
Oatlog: A performant ahead-of-time compiled e-graph engine by L. Gustafsson, E. Magnusson, and A.L. Cerpa was another talk I was really excited about. Basically they build a version of egglog, including the fancy relational e-matching, that does ahead-of-time optimization by assuming a fixed schema and set of rewrite rules. That lets them do a bunch of really fancy cross-rule optimization (like matching trie traversal orders) and get big speedups. Besides wanting to use this in Herbie (we've tried egglog and found that start-up times are too slow) I also like the idea that implementing "an egglog" is, again, doable and hope to see more alternatives and competition here. When multiple groups build the same kind of software they build a kind of distributed consensus about implementation strategies, algorithms, and optimizations that no single research group ever builds.
Omelets Need Onions: E-graphs Modulo Theories via Bottom Up E-Matching by P. Zucker was another highlight. I mean, I already feel like I am Phil's biggest fan, and by the way meeting him and talking in person was another big highlight of the trip, but still, this talk was a gem, starting from the hilarious opening through a really tightly presented version of his "bottom-up e-matching" idea. I particularly liked his "inner e-graph" example, which basically was the idea that you'd have a "theory" in an e-graph that decided equality between terms using another e-graph. Why would you want this? Uhh, no reason, I don't know, but I've thought about this exact hypothetical in my series on E-graphs modulo theories and Phil laid it out really well. Also I was supposed to miss this talk so I could be on a PLMW panel, but then I didn't want to miss the talk and ended up leaving early but still being late to PLMW. Sorry!
PLDI Day 1
Partial Evaluation, Whole-Program Compilation by C. Fallin and M. Bernstein1 [1 Who, funny story, I heard at least one attendee describe as "that guy with that great blog", well done Max!] was a great talk. The basic idea is pretty straightforward: transform a bytecode interpreter into a baseline compiler by doing a flow-sensitive compilation, where the flow-sensitivity captures the fact that you want to statically unroll the program counter while still symbolically evaluating the code itself. I mean, this is variation one million of Futamura projections and staging, but I enjoyed it, and I liked the framing as context and flow sensitivity (instead of as some kind of modal stage types). There were also a bunch of neat tricks in here, like collecting all the inline cache stubs from the benchmark suite, and it's super impressive that they applied this to Spidermonkey's bytecode compiler almost unchanged.
Exploiting Undefined Behavior in C/C++ Programs for Optimization: A Study on the Performance Impact by L. Popescu and N.P. Lopes is, for me, the most impressive paper in the whole conference. Nuno in particular has been doing fantastic work on C++ compiler correctness and undefined behavior for a long time now, fighting an incredibly important battle in a very challenging domain. I have to say, I do feel like the PL community as a whole, and even PLDI specifically, still do not give enough respect to work on actual widely-used programming languages. Real-world languages are messy in all sorts of ways, but I don't really jive with "washing our hands" of that mess and saying it's somehow not our fault or responsibility.
Anyway, undefined behavior is a real footgun in C and C++, and this paper asks whether exploiting that undefined behavior is actually necessary for performance. Or, to be more precise, necessary for performance in real-world code; there are simple micro-benchmarks where exploiting undefined behavior gives 2× or even bigger speed-ups, but it's unclear if that extends to "real code". Lucian and Nuno tested this by disabling some types of UB exploitation using flags and adding new flags to LLVM to disable more categories of it. Then they test a bunch of real-world programs using those programs' natural performance metrics (like frames per second for AV1 encoding).
The findings are super interesting: 1) yes, there are real-world slow-downs in meaningful amounts, about 5%;2 [2 Beware, the plots in the paper present this maybe a bit deceptively, focus on the rightmost point labeled "all".] and those slow-downs are widespread; 2) the slow-downs are greatly diminished by turning on LTO;3 [3 I can't find in the paper whether they mean full or thin so I assume they mean full, which unfortunately is kind of impractical.] and finally, 3) additional performance is recoverable by improving the existing optimizations and analyses within LLVM.
Is this an argument in favor of defining more of the C++ standard? Or
perhaps adding a -Osafe
or similar flag that defines more operations?
Maybe… What's interesting is that a lot of the optimizations, even
those that recover performance using LTO or better analyses, still
rely on things being undefined behavior, like overflowing a pointer or
having an unaligned field access. See section 6 of the paper for more
on this, it's pretty subtle. So I think this paper is more of an
argument in favor of "not exploiting" undefined behavior, maybe not in
favor of defining it. I don't know how to standardize that,
unfortunately, but it seems like a good avenue for future work.
Possibly some kind of "blame logic" where the compiler is allowed to
exploit UB only if the programmer is somehow to blame? I don't know.
But regardless, I felt like I learned a lot from this paper and this
talk about UB in real-world programs, and I in general think we in the
PL community should hold practical work like this in higher regard, so
well done Lucian and Nuno.
Slotted E-Graphs: First-Class Support for (Bound) Variables in E-Graphs by R. Schneider, M. Rossel, A. Shaikhha, A. Goens, T. Koehler, and M. Steuwer… I saw this talk earlier, at an Egraphs community meeting, and it was great to see this work finally published at PLDI. It's a pretty complicated paper—more than you'd think for such a simple topic, and some of the design choices are unintuitive—but I think it's also a really powerful part of the "Egraphs modulo T" discourse and possibly also a practical improvement to Egraphs for real-world code.
I chaired the session on numerics but, funny enough, paid too much attention to back-up questions, the timer, remembering speaker names and pronounciation, and so on, and as a result don't remember the actual talks in this session super well. Oops! They were good and I've read some of the papers but can't in good concience list them here. I think I spent the session after that talking to Phil, so that's all for day 1.
PLDI Day 2
Leo's keynote, Lean: Machine-Checked Mathematics and Verified Programming, Past and Future, was fantastic. I think the overall message was, why not just write all your software in Lean? It's got the best type system, it's really fast, it apparently supports everything you might want in a functional language… I'll have to retry Lean 5. I last used it I think five years ago, when I taught a few lectures on it, and it looks like it's changed a lot, with a whole set of powerful tactics and a new high-performance programming language.
Fast Direct Manipulation Programming with Patch-Reconciliation Correspondence by P. Ziegler, J. Lubin, and S.E. Chasins was a really great talk and also a good bit of theory around incremental computation. I'm increasingly convinced that incremental computation is the "ur-optimization" for GUI programming, and one that's still not super well understood and where the theory is really lacking. This talk highlighted, I would say, kind-of "light-weight" programming like in data analysis, visualization, GUIs, and so on. I think this area is under-explored. Previous work on incremental computing ran aground, I think, on the challenge of incrementalizing real data structures and algorithms, which turns out to be basically impossible. (You need to write new, incrementalization-friendly data structures and algorithms, and there's no reason to think that the incremental-friendly ones have the same asymptotics as the from-scratch ones.) But if the programs are fundamentally kind of light-weight, broad rather than deep, then it should be possible to cut out vast portions of the program when re-executing.
Tree Borrows by N. Villani, J. Hostert, D. Dreyer, and R. Jung, an actual Distinguished Paper, was also fantastic. This is another entry in my "more respect to real programming languages" list: the authors have been on a many-year journey to define the semantics of unsafe Rust, which is actually way way more complex than safe Rust because the whole point is to allow high-performance code. Tree borrows seems to allow that by "locking" and "unlocking" various accesses as code executes, basically ideas from program logic, and they have a very cool empirical evaluation of these rules by actually evaluating Rust code with the analysis running in real time, validating what is and isn't safe. I think the empirical evaluation adds a huge amount of value here, and it's a clever trick I hadn't previously seen in language design efforts that I'm really bullish on. More empirics for programming language semantics!
At this point I stepped out to hang out with old friends, so that's a wrap for day 2!
PLDI Day 3
Işıl's keynote, Neurosymbolic Program Synthesis: Bridging Perception and Reasoning in Real-World Applications, was very Işıl: a bunch of "just so" problems where the programming language, the synthesis technique, the analysis, and the machine learning all fit together perfectly. Every time I see one of these papers it seems so easy, but only Işıl constantly pulls it off. I don't know if the talk really sold me on the need for combined PL and ML approaches, and to be honest when I see papers like this I usually don't find them super insightful, but, again, Işıl's examples are just so perfectly designed that I definitely got the feeling of "yes, this is it" during the talk.
Usability Barriers for Liquid Types by C. Gamboa, A.E. Reese, A. Fonseca, and J. Aldrich was another great talk looking at practicalities. Honestly, a lot of the "usability barriers" they find are just the standard issues of research projects: hard to install, not enough documentation, not enough discussion of how to actually use it, and so on. I'm not sure there's necessarily a lesson here. Research projects are hard to transition to practice! And there's a lot of supporting infrastructure to build, like IDE support, autocomplete, installers, and so on. Perhaps I should spend some time learning LSP; possibly this (increasingly adopted) abstraction helps, I don't know much about it. The comments from experienced users were more interesting from a research point of view, especially on scalability and reliability for solvers, especially comparing to Leo's talk on Thursday. It seems, naively, like this should be solvable, but currently SMT solvers are more incentivized to solve harder constraint problems rather than focusing on predictability.
Conclusion
It was a great PLDI! I had a blast talking to people, trying to strike up collaborations, exchanging ideas. I was especially happy to see old friends, meet Phil in person for the first time, chat with Milind about batches for an hour, catch up with Ralf, Santosh, Ariel… Anyway, great to see everyone and looking forward to a year propelled by these meetings!
Footnotes:
Who, funny story, I heard at least one attendee describe as "that guy with that great blog", well done Max!
Beware, the plots in the paper present this maybe a bit deceptively, focus on the rightmost point labeled "all".
I can't find in the paper whether they mean full or thin so I assume they mean full, which unfortunately is kind of impractical.