License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2017.22
URN: urn:nbn:de:0030-drops-72667
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7266/
Podkopaev, Anton ;
Lahav, Ori ;
Vafeiadis, Viktor
Promising Compilation to ARMv8 POP
Abstract
We prove the correctness of compilation of relaxed memory accesses and release-acquire fences from the "promising" semantics of [Kang et al. POPL'17] to the ARMv8 POP machine of [Flur et al. POPL'16]. The proof is highly non-trivial because both the ARMv8 POP and the promising semantics provide some extremely weak consistency guarantees for normal memory accesses; however, they do so in rather different ways. Our proof of compilation correctness to ARMv8 POP strengthens the results of the Kang et al., who only proved the correctness of compilation to x86-TSO and Power, which are much simpler in comparison to ARMv8 POP.
BibTeX - Entry
@InProceedings{podkopaev_et_al:LIPIcs:2017:7266,
author = {Anton Podkopaev and Ori Lahav and Viktor Vafeiadis},
title = {{Promising Compilation to ARMv8 POP}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {22:1--22:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {Peter M{\"u}ller},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2017/7266},
URN = {urn:nbn:de:0030-drops-72667},
doi = {10.4230/LIPIcs.ECOOP.2017.22},
annote = {Keywords: ARM, Compilation Correctness, Weak Memory Model}
}
|
Keywords: |
|
ARM, Compilation Correctness, Weak Memory Model |
|
Collection: |
|
31st European Conference on Object-Oriented Programming (ECOOP 2017) |
|
Issue Date: |
|
2017 |
|
Date of publication: |
|
16.06.2017 |
