论文标题
使用isabelle/hol验证术语图优化
Verifying term graph optimizations using Isabelle/HOL
论文作者
论文摘要
我们的目标是正式验证GRAALVM编译器中使用的数百个表达优化规则的正确性。在定义编程语言的语义时，表达式自然形成抽象的语法树或术语。但是，为了促进共享常见子表达，现代编译器表示为术语图的表达式。定义术语图的语义比定义其等效术语表示的语义更为复杂。更重要的是，直接在术语图上定义优化并证明语义保存比等效术语表示要复杂得多。根据术语，优化可以表示为条件术语重写规则，并证明了重写是语义的保存相对简单的。在本文中，我们探讨了一种使用术语重写来验证GRAALVM编译器中优化的项图转换的方法。这种方法大大减少了整体验证工作，并可以更简单地编码优化规则。
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.
