Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Denotational Semantics of SSA

Jad Elkhaleq Ghalayini, Neel Krishnaswami

TL;DR

The paper develops a rigorous, type-theoretic treatment of SSA variants by introducing $\lambda_{\mathsf{SSA}}$, an equational theory, and a categorical denotational semantics rooted in Freyd-Elgot categories. It proves soundness and completeness with respect to the denotational model and demonstrates the practical viability of the framework through concrete models, including a $TSO$-weak-memory construction, with substantial Lean formalization. By bridging SSA with a rich semantic foundation and providing algorithmic conversions between SSA, ANF, and strict SSA, the work enables compositional, law-governed reasoning about compiler optimizations and memory models. The results provide a scalable toolkit for verifying SSA-level transformations and memory-model correctness, with broad implications for compiler verification and programmable memory semantics.

Abstract

Static single assignment form, or SSA, has been the dominant compiler intermediate representation for decades. In this paper, we give a type theory for a variant of SSA, including its equational theory, which are strong enough to validate a variety of control and data flow transformations. We also give a categorical semantics for SSA, and show that the type theory is sound and complete with respect to the categorical axiomatization. We demonstrate the utility of our model by exhibiting a variety of concrete models satisfying our axioms, including in particular a model of TSO weak memory. The correctness of the syntactic metatheory, as well as the completeness proof has been mechanized in the Lean proof assistant.

The Denotational Semantics of SSA

TL;DR

The paper develops a rigorous, type-theoretic treatment of SSA variants by introducing , an equational theory, and a categorical denotational semantics rooted in Freyd-Elgot categories. It proves soundness and completeness with respect to the denotational model and demonstrates the practical viability of the framework through concrete models, including a -weak-memory construction, with substantial Lean formalization. By bridging SSA with a rich semantic foundation and providing algorithmic conversions between SSA, ANF, and strict SSA, the work enables compositional, law-governed reasoning about compiler optimizations and memory models. The results provide a scalable toolkit for verifying SSA-level transformations and memory-model correctness, with broad implications for compiler verification and programmable memory semantics.

Abstract

Static single assignment form, or SSA, has been the dominant compiler intermediate representation for decades. In this paper, we give a type theory for a variant of SSA, including its equational theory, which are strong enough to validate a variety of control and data flow transformations. We also give a categorical semantics for SSA, and show that the type theory is sound and complete with respect to the categorical axiomatization. We demonstrate the utility of our model by exhibiting a variety of concrete models satisfying our axioms, including in particular a model of TSO weak memory. The correctness of the syntactic metatheory, as well as the completeness proof has been mechanized in the Lean proof assistant.

Paper Structure

This paper contains 43 sections, 31 theorems, 188 equations, 38 figures.

Table of Contents

  1. Introduction
  2. StaticSingleAssignmentForm
  3. TypeTheory
  4. Metatheory
  5. EquationalTheory
  6. Expressions
  7. Regions
  8. Metatheory
  9. StrictSSA
  10. From$\lambda_{\mathsf{SSA}}$toA-NormalForm
  11. FromANFtoSSA
  12. RecordsandEnums
  13. Böhm-JacopiniforSSA
  14. DenotationalSemantics
  15. FreydElgotCategories
  16. ...and 28 more sections

Key Result

lemma 1

Given$\Gamma\leq\Delta$,$\epsilon\leq\epsilon'$,and$\mathsf{L}\leq\mathsf{K}$,wehavethat:

Figures (38)

  • Figure 1: Asimple,slightlysuboptimalprogramtocompute$10!$viamultiplicationinaloop,represented astypicalimperativecodeandin3-addresscode.
  • Figure 2: ConversionofthreeaddresscodefortheprograminFigure \ref{['fig:fact-program']}toSSA form,requringtheinsertionof$\phi$-nodesfor$i$and$a$duetocontrol-flowdependent updates.NotehowSSA-formcanbeviewedas"threeaddresscodeinwhichall $\mathsf{let}$-bindingsareimmutable."
  • Figure 3: TheprograminFigure\ref{['fig:fact-program']}writteninstandardSSA(using$\phi$nodes), likeinLLVMllvm,andinbasic-blockswithargumentsSSA,likeinMLIRmlirand Craneliftcranelift.Thearguments$i_0,a_0$correspondingtothe$\phi$-nodes$i_0, a_0$arecoloredinredandblue,respectively.
  • Figure 4: ConversionofanSSAprogramfromdominance-basedscopingtoexplicitlexicalscoping
  • Figure 5: Allowingif-statementstojumptoarbitraryinstructions,ratherthanaterminator
  • ...and 33 more figures

Theorems & Definitions (42)

  • lemma 1: Weakening
  • lemma 2: Substitution
  • lemma 3: Labelsubstitution
  • lemma 4: Weakening(Rewriting)
  • lemma 5: Congruence(Substitution)
  • lemma 6: Congruence(LabelSubstitution)
  • lemma 7: name=A-normalization,restate=anfconversion
  • lemma 8: name=SSAconversion,restate=ssaconversion
  • lemma 9: name=PermutationInvariance,restate=cfgperminvar
  • lemma 10: name=CFGConversion,restate=cfgconversion
  • ...and 32 more