The Denotational Semantics of SSA
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.
Keywords
Cite
@article{arxiv.2411.09347,
title = {The Denotational Semantics of SSA},
author = {Jad Elkhaleq Ghalayini and Neel Krishnaswami},
journal= {arXiv preprint arXiv:2411.09347},
year = {2024}
}
Comments
95 pages, 38 figures, mechanization available at https://github.com/imbrem/debruijn-ssa/tree/toplas-artifact