Denotation-based Compositional Compiler Verification

TL;DR

This paper introduces a denotation-based framework for compiler verification that enhances compositionality by using semantic functions and behavior refinement, applicable to verifying compiler correctness incrementally.

Contribution

It proposes a novel denotational semantics approach with a semantic linking operator and refinement algebra, improving structured and compositional compiler verification.

Findings

Verified the front-end of CompCert using the framework.

Achieved effective compositional verification from sub-statements to entire programs.

Bridged the gap between theoretical semantics and practical compiler verification.

Abstract

A desired but challenging property of compiler verification is compositionality, in the sense that the compilation correctness of a program can be deduced incrementally from that of its substructures ranging from statements, functions, and modules. This article proposes a novel compiler verification framework based on denotational semantics for better compositionality, compared to previous approaches based on small-step operational semantics and simulation theories. Our denotational semantics is defined by semantic functions that map a syntactic component to a semantic domain composed of multiple behavioral \emph{sets}, with compiler correctness established through behavior refinement between the semantic domains of the source and target programs. The main contributions of this article include proposing a denotational semantics for open modules, a novel semantic linking operator, and a refinement algebra that unifies various behavior refinements, making compiler verification structured and compositional. Furthermore, our formalization captures the full meaning of a program and bridges the gap between traditional power-domain-based denotational semantics and the practical needs of compiler verification. We apply our denotation-based framework to verify the front-end of CompCert and typical optimizations on simple prototypes of imperative languages. Our results demonstrate that the compositionality from sub-statements to statements, from functions to modules, and from modules to the whole program can be effectively achieved.