A formal semantics of the GraalVM intermediate representation

DOI10.1007/978-3-030-88885-5_8MaRDI QIDQ2147184zbMATH OpenOpenAlexFDO

Authors Brae J. Webb, Mark Utting, Ian Hayes

Publication date 22 June 2022

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

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)

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.

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

Cites work

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

Cited in

(2)

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

Describes a project that uses

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)