Compositional Verification of Compiler Optimisations on Relaxed Memory

TL;DR

This paper introduces a denotational theory for verifying compiler optimisations on relaxed memory models like C++11, enabling compositional verification and implementation in a practical tool.

Contribution

It presents the first compositional verification method for optimisations under an axiomatic memory model, realized in a practical verification tool.

Findings

Verifies real-world optimisations under C++11 memory model

Enables compositional reasoning about optimisation validity

First push-button tool for such verification

Abstract

A valid compiler optimisation transforms a block in a program without introducing new observable behaviours to the program as a whole. Deciding which optimisations are valid can be difficult, and depends closely on the semantic model of the programming language. Axiomatic relaxed models, such as C++11, present particular challenges for determining validity, because such models allow subtle effects of a block transformation to be observed by the rest of the program. In this paper we present a denotational theory that captures optimisation validity on an axiomatic model corresponding to a fragment of C++11. Our theory allows verifying an optimisation compositionally, by considering only the block it transforms instead of the whole program. Using this property, we realise the theory in the first push-button tool that can verify real-world optimisations under an axiomatic memory model.