Static Single Assignment, or SSA, is a cornerstone of modern compiler design, on which projects such as the LLVM compiler infrastructure, GCC’s GIMPLE IR, Cranelift, and MLIR are based. One of the core advantages of putting programs in SSA form is the ability to reason about programs in a more equational manner: since variables always have exactly one definition, we can justify complex optimizations like global value numbering (which would otherwise need to take into account complex flow-sensitive definitions) and more easily implement various analyses.

One of the core observations of the MLIR project is that SSA is very widely applicable, being useful for representing everything from high-level machine learning operations to low-level GPU code, and even hardware designs, as in the CIRCT project. This hints that SSA is a natural syntax for some fundamental compositional structure, much like how the simply typed lambda calculus is a natural syntax for Cartesian closed categories.

In this talk, we would like to argue that SSA without control-flow is a syntax for Freyd categories, which we then provide a graphical syntax for in terms of string diagrams as in (Román, Promonads and String Diagrams for Effectful Categories, 2022). We then argue that SSA with terminating control-flow (i.e., in which the basic blocks form a DAG) corresponds exactly to distributive Freyd categories, while SSA with general control-flow corresponds to equipping a distributive Freyd category with an Elgot structure; we then give a string-diagrammatic graphical representation of such programs based on traditional control-flow graphs.

We do this by providing a type-theoretic presentation of SSA, which we call isotope-SSA, which is designed to be amenable to inductive proofs and definitions. By using this formalization, we can equip SSA with a categorical semantics, which we show satisfies important properties such as semantic substitution and congruence. We then show how various optimizations, such as strength reduction, constant propagation, global value numbering, loop hoisting, and E-graph rewriting are compatible with our semantics. Finally, we give various models of our categorical semantics exhibiting interesting features, building up to a simple model of TSO-style weak memory based on (Kavanagh and Brookes, A Denotational Semantics for SPARC TSO, 2018) which treats the interactions between threads in a compositional manner.

Time permitting, we also hope to explain how to generalize our IR with support for substructural types and impure substitutions based on Führmann’s notion of central, copyable, and discardable programs (Führmann, Direct models of the computational lambda-calculus, 1999), which requires us to move to the more general setting of distributive effectful categories, and give a few applications of this more general system relating to separation logic, quantum computing, and nondeterminism.

PhD student at the Department of Computer Science and Technology in the University of Cambridge, supervised by Neel Krishnaswami.