AxCut: A Safe Intermediate Language for Fast, Ubiquitous Asynchrony

Historically, programming languages and their intermediate representations have been designed and optimized to excel at batch computing. However, modern programs are increasingly interactive. They interact not only with the outside world through input and output devices but also with specialized computation devices like GPUs or TPUs, which perform computation-intensive tasks. In both cases, to prevent programs from becoming unresponsive, computation needs to be suspended without blocking other computations from being performed. In other words, communication with these devices must be asynchronous. Over the last few decades, these requirements have led to new programming paradigms, new programming languages, and now necessitate new intermediate representations.

The goal of the proposed research project is thus to develop a new kind of intermediate representation: AxCut. It will be built from the ground up to facilitate compiler development for asynchronous programming paradigms. This stands in contrast to many existing academic and industrial intermediate representations, which have added support for asynchrony only as an afterthought, if at all. By taking inspiration from classical sequent calculus, AxCut will not only be well-suited to represent and optimize asynchronous programs, but also to formally reason about their correctness. All of this ultimately serves to make software more reliable and more responsive, addressing the challenges of today’s reality of pervasive asynchrony.