. "This paper is about verifying program transformations on an axiomatic\r\nrelaxed memory model of the kind used in C/C++ and Java. Relaxed models\r\npresent particular challenges for verifying program transformations, because\r\nthey generate many additional modes of interaction between code and context.\r\nFor a block of code being transformed, we define a denotation from its behaviour\r\nin a set of representative contexts. Our denotation summarises interactions of the\r\ncode block with the rest of the program both through local and global variables,\r\nand through subtle synchronisation effects due to relaxed memory. We can then\r\nprove that a transformation does not introduce new program behaviours by comparing\r\nthe denotations of the code block before and after. Our approach is compositional:\r\nby examining only representative contexts, transformations are verified\r\nfor any context. It is also fully abstract, meaning any valid transformation can be\r\nverified. We cover several tricky aspects of C/C++-style memory models, including\r\nrelease-acquire operations, sequentially consistent fences, and non-atomics.\r\nWe also define a variant of our denotation that is finite at the cost of losing full\r\nabstraction. Based on this variant, we have implemented a prototype verification\r\ntool and app"^^ . . . . . . . . . . . . . . . . . . "2018-04-14" . . . "10801" . . . . . "Compositional Verification of Compiler Optimisations on Relaxed Memory"^^ . . . .