Document Open Access Logo

Promising Compilation to ARMv8 POP

Authors Anton Podkopaev, Ori Lahav, Viktor Vafeiadis

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2017.22.pdf
  • Filesize: 0.69 MB
  • 28 pages

Document Identifiers

Author Details

Anton Podkopaev
Ori Lahav
Viktor Vafeiadis

Cite As Get BibTex

Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis. Promising Compilation to ARMv8 POP. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 22:1-22:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.ECOOP.2017.22

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.

Subject Classification

Keywords
  • ARM
  • Compilation Correctness
  • Weak Memory Model

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. ARM architecture reference manual: ARMv8, for ARMv8-A architecture profile. Available at https://developer.arm.com/docs/ddi0487/latest/arm-architecture-reference-manual-armv8-for-armv8-a-architecture-profile [Online; accessed 16-May-2017].
  2. C/C++11 mappings to processors. Available at https://www.cl.cam.ac.uk/~pes20/cpp/cpp0xmappings.html. [Online; accessed 16-May-2017].
  3. The herdtools7 repository. Available at https://github.com/herd/herdtools7 [Online; accessed 16-May-2017].
  4. Martín Abadi and Leslie Lamport. The existence of refinement mappings. Theor. Comput. Sci., 82(2):253-284, 1991. URL: http://dx.doi.org/10.1109/LICS.1988.5115.
  5. Jade Alglave, Luc Maranget, and Michael Tautschnig. Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst., 36(2):7:1-7:74, 2014. URL: http://dx.doi.org/10.1145/2627752.
  6. Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, and Peter Sewell. The problem of programming language concurrency semantics. In ESOP, volume 9032 of LNCS, pages 283-307. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-46669-8_12.
  7. Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. Mathematizing C++ concurrency. In POPL 2011, pages 55-66. ACM, 2011. URL: http://dx.doi.org/10.1145/1925844.1926394.
  8. Hans-J. Boehm and Brian Demsky. Outlawing ghosts: Avoiding out-of-thin-air results. In MSPC 2014, pages 7:1-7:6. ACM, 2014. URL: http://dx.doi.org/10.1145/2618128.2618134.
  9. Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter Sewell. Modelling the ARMv8 architecture, operationally: Concurrency and ISA. In POPL 2016, pages 608-621. ACM, 2016. URL: http://dx.doi.org/10.1145/2837614.2837615.
  10. John L. Hennessy and David A. Patterson. Computer Architecture - A Quantitative Approach (5. ed.). Morgan Kaufmann, 2012. Google Scholar
  11. Alan Jeffrey and James Riely. On thin air reads: Towards an event structures model of relaxed memory. In LICS 2016. IEEE, 2016. URL: http://dx.doi.org/10.1145/2933575.2934536.
  12. Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer. A promising semantics for relaxed-memory concurrency. In POPL 2017. ACM, 2017. URL: http://dx.doi.org/10.1145/3009837.3009850.
  13. Ori Lahav and Viktor Vafeiadis. Explaining relaxed memory models with program transformations. In FM 2016. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-319-48989-6_29.
  14. Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer. Repairing sequential consistency in C/C++11. In PLDI 2017. ACM, 2017. Google Scholar
  15. Leslie Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Computers, 28(9):690-691, 1979. URL: http://dx.doi.org/10.1109/TC.1979.1675439.
  16. Nancy Lynch and Frits Vaandrager. Forward and backward simulations: I. Untimed systems. Inf. Comput., 121(2):214-233, 1995. URL: http://dx.doi.org/10.1006/inco.1995.1134.
  17. Yatin A. Manerkar, Caroline Trippel, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. Counterexamples and proof loophole for the C/C++ to POWER and ARMv7 trailing-sync compiler mappings. CoRR, abs/1611.01507, 2016. URL: http://arxiv.org/abs/1611.01507.
  18. Jeremy Manson, William Pugh, and Sarita V. Adve. The Java memory model. In POPL 2005, pages 378-391. ACM, 2005. URL: http://dx.doi.org/10.1145/1040305.1040336.
  19. Jean Pichon-Pharabod and Peter Sewell. A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions. In POPL 2016, pages 622-633. ACM, 2016. URL: http://dx.doi.org/10.1145/2837614.2837616.
  20. Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis. Promising compilation to ARMv8 POP. Extended version, 2017. Available at http://podkopaev.net/armpromise [Online; accessed 16-May-2017].
  21. Anton Podkopaev, Ilya Sergey, and Aleksandar Nanevski. Operational aspects of C/C++ concurrency. CoRR, abs/1606.01400, 2016. URL: http://arxiv.org/abs/1606.01400.
  22. Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, and Derek Williams. Understanding POWER multiprocessors. In PLDI 2011, pages 175-186. ACM, 2011. URL: http://dx.doi.org/10.1145/1993498.1993520.
  23. Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, and Magnus O. Myreen. x86-TSO: A rigorous and usable programmer’s model for x86 multiprocessors. Commun. ACM, 53(7):89-97, 2010. URL: http://dx.doi.org/10.1145/1785414.1785443.
  24. John Wickerson, Mark Batty, Tyler Sorensen, and George A. Constantinides. Automatically comparing memory consistency models. In POPL 2017. ACM, 2017. URL: http://dx.doi.org/10.1145/3009837.3009838.
  25. Yang Zhang and Xinyu Feng. An operational happens-before memory model. Frontiers of Computer Science, 10(1):54-81, 2016. URL: http://dx.doi.org/10.1007/s11704-015-4492-4.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact