PLDI is one of the marquee programming languages conference and one my favorite ones to attend. The number of domains that PL are working in and bringing ideas to is frankly overwhelming and inspiring. I had a bunch of interesting conversations that incited new ideas and perspectives for me.

For the Masses or for the FLOPs?

Building and programming heterogenous systems has quickly become one of the key problems being tackled by the systems community. For the PL community, this should present tons of interesting work on defining programming models for emerging accelerators (GPUs, TPUs) and programming large systems that use them. Given this, I was surprised by the lack of papers tackling these problems.

After several long conversations with other conference attendees, I came up with the following framing. Programming languages research has two models of impact: building for the masses or building for the FLOPs (floating-point operations). A vast majority of the FLOPs in the world today come from specialized hardware like GPUs and TPUs. These accelerators generally use highly specialized programming models like CUDA or high-level languages like PyTorch. On the other hand, a vast majority of programmers use general-purpose languages like Python or JavaScript.

As a PL researcher, this poses a problem: you can work on building programming systems that enable more people to effectively interface with computers, or you could build better interfaces to a vast majority of the computation in the world. I think the current iteration of the PLDI community focuses on the former problem–of building better programming systems for the most number of people–while conferences like ASPLOS publish a lot more of the work on the latter kinds of problems. For example, the PyTorch 2 paper was published at ASPLOS ’24.

Like most distinctions, I don’t think this is a black-and-white divide but I did find this to be a useful lens to look through.

Tools for Language Evolution

Turning to general-purpose languages, the new RPLS workshop and Sukyong Ryu’s keynote highlighted the need for tools for language evolution. There has been a lot of work in the community on building tools that help specify formal semantics of languages and automatically generate tools like interpreters, symbolic verifiers, etc. Instead of trying to use general-purpose semantics specification tools like the K framework, Sukyong’s group has developed language specific tools: ESMeta for JavaScript, and SpecTec for WASM and worked hard to integrate into the community’s workflow. For example, the JavaScript community already had an English-language specification for operations like addition that are written with a precise pseudocode language. It would be a drastic change of norms (and a huge waste) to throw out these specifications. ESMeta provides a formal specification language to describe JavaScript (or, as it is officially called, ECMAScript) and automatically generates the same English-language documentation. This means that the community can move towards a formal, single source of truth model for defining the language and keeping it up-to-date.

These kinds of single-source of truth language specifications seem to only be growing in importance. The WASM community adopted the SpecTec project (also from Sukyong’s group), ARM defines the ISA semantics using the architecture specification language (ASL) and the SAIL architecture specification language has been successfully used to define the semantics of ISAs like ARM-A, x86, IBM Power, and CHERI.

Formal Verification Looms Large

Formal verification of systems, languages, and semantics remains one of the primary focuses of PLDI. Two out of the six distinguished papers focused on formal verification of some form and Leo de Moura gave a keynote on the Lean project. The talk went over the wide impact Lean has had over the mathematics and the software engineering community. There were two projects that I particularly found interesting:

• The mathlib project which has slowly accumulated theorems and proofs from algebra, geometry, and analysis. The project provides a large number of building blocks for anyone interested in writing sophisticated mathematical proofs (like Terrance Tao’s proof of the PFR conjecture).
• The Veil Framework by folks at NUS which provides a domain-specific language verifying distributed algorithms. The cool thing about Veil is that because it is embedded within Lean, it can provide both automatic and deductive verification. The former uses SMT solver integration to perform proof search while the latter uses the Lean proof assistant to generate proofs through tactics. Furthermore, because Lean has extensive metaprogramming support, Veil programs actually look more like Alloy or TLA+ programs than like other Leans.

These two projects, to me, provide an existence proof for the potential of designing large-scale hardware-software verification stacks within Lean. For example, think of a system that takes proofs about computations on fully homomorphically encrypted data and connects them all the way down to the hardware while allowing domain experts to use abstractions they’re familiar and comfortable with!

Papers

The main conference has several parallel tracks so I couldn’t see all the talks I wanted to but here is a collection of talks I found interesting:

• Making Concurrent Hardware Verification Sequential: Normally, when thinking about the behavior of a processor, we like to think of a sequential implementation–an interpreter that run each instruction one at a time–as the ideal behavior of the processor. Pipelining, speculation, out-of-order execution all must be shown to be refinement of (i.e., admitting fewer behaviors than) this sequential implementation. This feels like a pretty reasonable model and exactly how I thought of processors. However, this paper shows that it is not actually possible to connect purely sequential implementations to more complex processors! The crux of the problem is that a real processor might, for example, have multiple memory requests in-flight before the first one returns, which is a behavior that the sequential implementation cannot exhibit but a pipelined one might. I find this result pretty staggering and am very interested in diving into the details.
• Bean: A Language for Backward Error Analysis: The talk presented a type system to quantify the backward error present in a program due to floating-point errors (compared to a corresponding real-valued computation). I found this to be a really cool combination of deep theory work (to make the notion of compositional error analysis work) and application focused ideas (error analysis is done very manually and seems to be very tedious). The paper presents a limited language with quite a few restrictions (which are justified and analyzed by the theory) but to me, the interesting part was that this is even possible at all. The talk is well worth a watch when it shows up on the SIGPLAN channel.
• Task-Based Tensor Computations on Modern GPUs: One of the only talks about GPU programming. Beyond the research contributions, I found the talk to be a pretty lucid description of the current programming model for GPUs (which is kind of insane and cool). The crux of the problem is that the newest NVIDIA GPUs have an asynchronous execution interface for the tensor cores (circuits that perform matrix-multiply) and the processor cores (streaming multi-processors) need to find work to do while the tensor cores are doing their thing. The standard SIMT programming model makes it hard to find and do said work so the task-based approach makes a lot more sense.
• MISAAL: Synthesis-Based Automatic Generation of Efficient and Retargetable Semantics-Driven Optimizations. MISAAL continues in the line of work from Vikram Adve’s group on automatically synthesizing compilers from ISA specifications. The work has a lot of moving pieces so I’ll leave the details to the paper but one thing I found to be interesting was that the authors parsed the pseudocode language used by different ISA vendors to generate specifications for ISA instructions! This is a pretty good example where specification languages like ASL can be useful in rapidly enabling this kind of work.

Conclusion

The golden age of computer architecture continues and with it, heterogeneity remains one of the most interesting and challenging programming problems. I continue to think that the toolset developed by the PL community is extremely well-suited to address these problems and I’m excited to see what folks build next!