A formal semantics of the GraalVM intermediate representation

DOI10.1007/978-3-030-88885-5_8zbMATH Open1497.68104arXiv2107.01815OpenAlexW3209237303MaRDI QIDQ2147184FDOQ2147184

Authors: Brae J. Webb, Mark Utting, Ian Hayes 

Publication date: 22 June 2022

Abstract: 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.

Full work available at URL: https://arxiv.org/abs/2107.01815

Recommendations

• Formalizing the LLVM intermediate representation for verified program transformations
• Types for Proofs and Programs
• Abstract State Machines 2004. Advances in Theory and Practice
• A Framework for Formal Verification of Compiler Optimizations
• A verifiable SSA program representation for aggressive compiler optimization

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Semantics in the theory of computing (68Q55) Formalization of mathematics in connection with theorem provers (68V20)

Cites Work

• Formalizing the LLVM intermediate representation for verified program transformations
• Isabelle/HOL. A proof assistant for higher-order logic
• CakeML
• The program dependence graph and its use in optimization
• Mechanising a type-safe model of multithreaded Java with a verified compiler
• Heaps and Data Structures: A Challenge for Automated Provers

Cited In (2)

• Engineering a common intermediate representation for the Ovm framework
• Abstract State Machines 2004. Advances in Theory and Practice

Uses Software

• Isabelle/HOL
• LLVM
• CakeML
• CompCert
• Vellvm
• GitHub
• GraalVM

This page was built for publication: A formal semantics of the GraalVM intermediate representation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2147184)