This HTML5 document contains 31 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dctermshttp://purl.org/dc/terms/
n7doi:10.1007/
n2https://kar.kent.ac.uk/id/eprint/
wdrshttp://www.w3.org/2007/05/powder-s#
dchttp://purl.org/dc/elements/1.1/
n10http://purl.org/ontology/bibo/status/
rdfshttp://www.w3.org/2000/01/rdf-schema#
n12https://kar.kent.ac.uk/id/subject/
n9https://demo.openlinksw.com/about/id/entity/https/raw.githubusercontent.com/annajordanous/CO644Files/main/
n3http://eprints.org/ontology/
n16https://kar.kent.ac.uk/66630/
n13https://kar.kent.ac.uk/id/event/
bibohttp://purl.org/ontology/bibo/
n14https://kar.kent.ac.uk/id/publication/
n20https://kar.kent.ac.uk/id/eprint/66630#
n18https://kar.kent.ac.uk/id/org/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
owlhttp://www.w3.org/2002/07/owl#
n4https://kar.kent.ac.uk/id/document/
n21https://kar.kent.ac.uk/id/
xsdhhttp://www.w3.org/2001/XMLSchema#
n19https://demo.openlinksw.com/about/id/entity/https/www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/
n17https://kar.kent.ac.uk/id/person/

Statements

Subject Item
n2:66630
rdf:type
bibo:Article bibo:AcademicArticle n3:EPrint n3:ConferenceItemEPrint
rdfs:seeAlso
n16:
owl:sameAs
n7:978-3-319-89884-1_36
n3:hasAccepted
n4:1033008
n3:hasDocument
n4:1033008 n4:1262479 n4:1666124 n4:1666121 n4:1666122 n4:1666123
dc:hasVersion
n4:1033008
dcterms:title
Compositional Verification of Compiler Optimisations on Relaxed Memory
wdrs:describedby
n9:export_kar_RDFN3.n3 n19:export_kar_RDFN3.n3
dcterms:date
2018-04-14
dcterms:creator
n17:ext-m.j.batty@kent.ac.uk n17:ext-fbfdc71228b85aef8917e64204399e71 n17:ext-1396ca13a8f47826f5b221ebb47ee6f4
bibo:status
n10:peerReviewed n10:published
dcterms:publisher
n18:ext-1c5ddec173ca8cdfba8b274309638579
bibo: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
dcterms:isPartOf
n14:ext-03029743 n21:repository
dcterms:subject
n12:QA75
bibo:authorList
n20:authors
bibo:presentedAt
n13:ext-1dfb8cb2333f890db199b62ea5f85714
bibo:volume
10801