Compositional Verification of Compiler Optimisations on Relaxed Memory

Dodds, Mike and Batty, Mark and Gotsman, Alexey (2018) Compositional Verification of Compiler Optimisations on Relaxed Memory. In: ESOP 2018, April 14-20, 2018, Thessaloniki, Greece. (doi:https://doi.org/10.1007/978-3-319-89884-1_36) (Full text available)

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)
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 75 Electronic computers. Computer science
Divisions: Faculties > Sciences > School of Computing
Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Mark Batty
Date Deposited: 05 Apr 2018 14:36 UTC
Last Modified: 11 Jun 2018 14:38 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