Compositional Verification of Compiler Optimisations on Relaxed Memory

Mike Dodds, Mark Batty, Alexey Gotsman

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…