The Denotational Semantics of SSA

TL;DR

This paper develops a formal type theory and categorical semantics for SSA, validating control and data flow transformations, and demonstrates its applicability including modeling TSO weak memory.

Contribution

It introduces a formal type theory and categorical semantics for SSA, with mechanized proofs, and models weak memory systems.

Findings

Type theory for SSA validated control and data flow transformations.

Categorical semantics for SSA established, including TSO weak memory model.

Mechanized proofs of correctness and completeness in Lean.

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.