Compositional Verification of Compiler Optimisations on Relaxed Memory

This paper is about verifying program transformations on an axiomatic

relaxed memory model of the kind used in C/C++ and Java. Relaxed models

present particular challenges for verifying program transformations, because

they generate many additional modes of interaction between code and context.

For a block of code being transformed, we define a denotation from its behaviour

in a set of representative contexts. Our denotation summarises interactions of the

code block with the rest of the program both through local and global variables,

and through subtle synchronisation effects due to relaxed memory. We can then

prove that a transformation does not introduce new program behaviours by comparing

the denotations of the code block before and after. Our approach is compositional:

by examining only representative contexts, transformations are verified

for any context. It is also fully abstract, meaning any valid transformation can be

verified. We cover several tricky aspects of C/C++-style memory models, including

release-acquire operations, sequentially consistent fences, and non-atomics.

We also define a variant of our denotation that is finite at the cost of losing full

abstraction. Based on this variant, we have implemented a prototype verification

tool and app