Skip to main content
Kent Academic Repository

Compositional Verification of Compiler Optimisations on Relaxed Memory

Dodds, Mike, Batty, Mark, Gotsman, Alexey (2018) Compositional Verification of Compiler Optimisations on Relaxed Memory. In: Lecture Notes in Computer Science. Programming Languages and Systems: 27th European Symposium on Programming, ESOP 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018 Proceedings. 10801. Springer ISBN 978-3-319-89883-4. (doi:10.1007/978-3-319-89884-1_36) (KAR id:66630)

Abstract

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

Item Type: Conference or workshop item (Proceeding)
DOI/Identification number: 10.1007/978-3-319-89884-1_36
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 75 Electronic computers. Computer science
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Batty
Date Deposited: 05 Apr 2018 14:36 UTC
Last Modified: 04 Mar 2024 19:00 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/66630 (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.