The Denotational Semantics of SSA
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909425132896256 |
|---|---|
| author | Ghalayini, Jad Elkhaleq Krishnaswami, Neel |
| author_facet | Ghalayini, Jad Elkhaleq Krishnaswami, Neel |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_09347 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | The Denotational Semantics of SSA Ghalayini, Jad Elkhaleq Krishnaswami, Neel Programming Languages Logic in Computer Science F.3.2; D.3.4; D.3.1 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. |
| title | The Denotational Semantics of SSA |
| topic | Programming Languages Logic in Computer Science F.3.2; D.3.4; D.3.1 |
| url | https://arxiv.org/abs/2411.09347 |