License
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://drops.dagstuhl.de/opus/volltexte/2017/7266/
Go to the corresponding LIPIcs Volume Portal


Podkopaev, Anton ; Lahav, Ori ; Vafeiadis, Viktor

Promising Compilation to ARMv8 POP

pdf-format:
LIPIcs-ECOOP-2017-22.pdf (0.7 MB)


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
Seminar: 31st European Conference on Object-Oriented Programming (ECOOP 2017)
Issue Date: 2017
Date of publication: 13.06.2017


DROPS-Home | Fulltext Search | Imprint Published by LZI