Verifying term graph optimizations using Isabelle/HOL

TL;DR

This paper presents a formal verification approach for compiler optimizations on term graphs using Isabelle/HOL, simplifying the proof process and ensuring correctness within GraalVM.

Contribution

It introduces a method to verify term graph transformations via term rewrites, reducing complexity compared to direct graph verification.

Findings

Verification of optimizations is more straightforward on terms than on graphs.

Using term rewrites simplifies the proof process for semantics preservation.

The approach effectively verifies hundreds of GraalVM compiler optimization rules.

Abstract

Our objective is to formally verify the correctness of the hundreds of expression optimization rules used within the GraalVM compiler. When defining the semantics of a programming language, expressions naturally form abstract syntax trees, or, terms. However, in order to facilitate sharing of common subexpressions, modern compilers represent expressions as term graphs. Defining the semantics of term graphs is more complicated than defining the semantics of their equivalent term representations. More significantly, defining optimizations directly on term graphs and proving semantics preservation is considerably more complicated than on the equivalent term representations. On terms, optimizations can be expressed as conditional term rewriting rules, and proofs that the rewrites are semantics preserving are relatively straightforward. In this paper, we explore an approach to using term rewrites to verify term graph transformations of optimizations within the GraalVM compiler. This approach significantly reduces the overall verification effort and allows for simpler encoding of optimization rules.