Skip to main content

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)

PDF - Author's Accepted Manuscript
Download (618kB) Preview
[img]
Preview
Official URL
https://doi.org/10.1007/978-3-319-89884-1_36

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: Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Mark Batty
Date Deposited: 05 Apr 2018 14:36 UTC
Last Modified: 09 Jul 2019 11:21 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/66630 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year