A Formal Semantics of the GraalVM Intermediate Representation
Fuente:
arXiv
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2021
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866916142475378688 |
|---|---|
| author | Webb, Brae J. Utting, Mark Hayes, Ian J. |
| author_facet | Webb, Brae J. Utting, Mark Hayes, Ian J. |
| contents | The optimization phase of a compiler is responsible for transforming an intermediate representation (IR) of a program into a more efficient form. Modern optimizers, such as that used in the GraalVM compiler, use an IR consisting of a sophisticated graph data structure that combines data flow and control flow into the one structure. As part of a wider project on the verification of optimization passes of GraalVM, this paper describes a semantics for its IR within Isabelle/HOL. The semantics consists of a big-step operational semantics for data nodes (which are represented in a graph-based static single assignment (SSA) form) and a small-step operational semantics for handling control flow including heap-based reads and writes, exceptions, and method calls. We have proved a suite of canonicalization optimizations and conditional elimination optimizations with respect to the semantics. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2107_01815 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | A Formal Semantics of the GraalVM Intermediate Representation Webb, Brae J. Utting, Mark Hayes, Ian J. Logic in Computer Science Programming Languages The optimization phase of a compiler is responsible for transforming an intermediate representation (IR) of a program into a more efficient form. Modern optimizers, such as that used in the GraalVM compiler, use an IR consisting of a sophisticated graph data structure that combines data flow and control flow into the one structure. As part of a wider project on the verification of optimization passes of GraalVM, this paper describes a semantics for its IR within Isabelle/HOL. The semantics consists of a big-step operational semantics for data nodes (which are represented in a graph-based static single assignment (SSA) form) and a small-step operational semantics for handling control flow including heap-based reads and writes, exceptions, and method calls. We have proved a suite of canonicalization optimizations and conditional elimination optimizations with respect to the semantics. |
| title | A Formal Semantics of the GraalVM Intermediate Representation |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2107.01815 |