Document Open Access Logo

Reconciling Event Structures with Modern Multiprocessors

Authors Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, Viktor Vafeiadis

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2020.5.pdf
  • Filesize: 0.64 MB
  • 26 pages

Document Identifiers

Author Details

Evgenii Moiseenko
  • St. Petersburg State University, Russia
  • JetBrains Research, St. Petersburg, Russia
Anton Podkopaev
  • National Research University Higher School of Economics, Moscow, Russia
  • MPI-SWS, Kaiserslautern, Germany
  • JetBrains Research, St. Petersburg, Russia
Ori Lahav
  • Tel Aviv University, Israel
Orestis Melkonian
  • University of Edinburgh, UK
Viktor Vafeiadis
  • MPI-SWS, Kaiserslautern, Germany

Funding

  • Moiseenko, Evgenii: was supported by RFBR (grant number 18-01-00380).
  • Podkopaev, Anton: was supported by RFBR (grant number 118-01-00380).
  • Lahav, Ori: was supported by the Israel Science Foundation (grant number 5166651), by Len Blavatnik and the Blavatnik Family foundation, and by the Alon Young Faculty Fellowship.

Cite AsGet BibTex

Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, and Viktor Vafeiadis. Reconciling Event Structures with Modern Multiprocessors. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 5:1-5:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.ECOOP.2020.5

Abstract

Weakestmo is a recently proposed memory consistency model that uses event structures to resolve the infamous "out-of-thin-air" problem and to enable efficient compilation to hardware. Nevertheless, this latter property - compilation correctness - has not yet been formally established. This paper closes this gap by establishing correctness of the intended compilation schemes from Weakestmo to a wide range of formal hardware memory models (x86, POWER, ARMv7, ARMv8) in the Coq proof assistant. Our proof is the first that establishes correctness of compilation of an event-structure-based model that forbids "out-of-thin-air" behaviors, as well as the first mechanized compilation proof of a weak memory model supporting sequentially consistent accesses to such a range of hardware platforms. Our compilation proof goes via the recent Intermediate Memory Model (IMM), which we suitably extend with sequentially consistent accesses.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Software and its engineering → Concurrent programming languages
Keywords
  • Weak Memory Consistency
  • Event Structures
  • IMM
  • Weakestmo

Metrics

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

Related Versions

Supplementary Materials

References

  1. 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, July 2014. URL: https://doi.org/10.1145/2627752.
  2. Mark Batty, Alastair F. Donaldson, and John Wickerson. Overhauling SC atomics in C11 and OpenCL. In POPL 2016, pages 634-648. ACM, 2016. Google Scholar
  3. Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. Mathematizing C++ concurrency. In POPL 2011, pages 55-66, New York, 2011. ACM. URL: https://doi.org/10.1145/1925844.1926394.
  4. John Bender and Jens Palsberg. A formalization of java’s concurrent access modes. Proc. ACM Program. Lang., 3(OOPSLA):142:1-142:28, October 2019. URL: https://doi.org/10.1145/3360568.
  5. 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: https://doi.org/10.1145/2618128.2618134.
  6. Soham Chakraborty and Viktor Vafeiadis. Grounding thin-air reads with event structures. Proc. ACM Program. Lang., 3(POPL):70:1-70:27, 2019. URL: https://doi.org/10.1145/3290383.
  7. The Coq development of IMM, available at http://github.com/weakmemory/imm, 2019.
  8. Stephen Dolan, KC Sivaramakrishnan, and Anil Madhavapeddy. Bounding data races in space and time. In PLDI 2018, pages 242-255, New York, 2018. ACM. URL: https://doi.org/10.1145/3192366.3192421.
  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, New York, 2016. ACM. URL: https://doi.org/10.1145/2837614.2837615.
  10. Alan Jeffrey and James Riely. On thin air reads towards an event structures model of relaxed memory. In LICS 2016, pages 759-767, New York, 2016. ACM. URL: https://doi.org/10.1145/2933575.2934536.
  11. Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer. A promising semantics for relaxed-memory concurrency. In POPL 2017, pages 175-189, New York, 2017. ACM. URL: https://doi.org/10.1145/3009837.3009850.
  12. Ori Lahav and Viktor Vafeiadis. Explaining relaxed memory models with program transformations. In FM 2016. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-48989-6_29.
  13. Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer. Repairing sequential consistency in C/C++11. In PLDI 2017, pages 618-632, New York, 2017. ACM. URL: https://doi.org/10.1145/3062341.3062352.
  14. Jeremy Manson, William Pugh, and Sarita V. Adve. The Java memory model. In POPL 2005, pages 378-391, New York, 2005. ACM. URL: https://doi.org/10.1145/1040305.1040336.
  15. C/C++11 mappings to processors, 2016. URL: http://www.cl.cam.ac.uk/~pes20/cpp/cpp0xmappings.html.
  16. Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, and Viktor Vafeiadis. Coq proof scripts and supplementary material for this paper, available at http://plv.mpi-sws.org/weakestmoToImm/, 2020.
  17. Scott Owens, Susmit Sarkar, and Peter Sewell. A better x86 memory model: x86-TSO. In TPHOLs 2009, volume 5674 of LNCS, pages 391-407, Heidelberg, 2009. Springer. Google Scholar
  18. 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, New York, 2016. ACM. URL: https://doi.org/10.1145/2837614.2837616.
  19. Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis. Bridging the gap between programming languages and hardware weak memory models. Proc. ACM Program. Lang., 3(POPL):69:1-69:31, 2019. URL: https://doi.org/10.1145/3290382.
  20. 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.
  21. Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell. Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8. Proc. ACM Program. Lang., 2(POPL):19:1-19:29, 2018. URL: https://doi.org/10.1145/3158107.
  22. Christopher Pulte, Jean Pichon-Pharabod, Jeehoon Kang, Sung-Hwan Lee, and Chung-Kil Hur. Promising-ARM/RISC-V: a simpler and faster operational concurrency model. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, pages 1-15, New York, NY, USA, 2019. ACM. URL: https://doi.org/10.1145/3314221.3314624.
  23. Jaroslav Ševčík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, and Peter Sewell. CompCertTSO: A verified compiler for relaxed-memory concurrency. J. ACM, 60(3):22, 2013. URL: https://doi.org/10.1145/2487241.2487248.
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 Imprint Privacy Contact