Document Open Access Logo

Reconciling Event Structures with Modern Multiprocessors (Artifact)

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

PDF
Thumbnail PDF

Artifact Description

DARTS.6.2.4.pdf
  • Filesize: 267 kB
  • 3 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

Acknowledgements

We would like to thank the reviewers from the ECOOP Artifact Evaluation Committee for their time spent on evaluation of our artifact and for their feedback.

Cite AsGet BibTex

Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, and Viktor Vafeiadis. Reconciling Event Structures with Modern Multiprocessors (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 4:1-4:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/DARTS.6.2.4

Artifact

Abstract

The artifact is a virtual machine image containing two Coq packages which include mechanization of proofs stated in the paper. The first package imm contains a modified version of the Intermediate Memory Model, extended with the support of sequentially consistent atomics, and the compilation correctness proofs from it to hardware models. The second package weakestmoToImm contains a definition of the Weakestmo memory model as well as a compilation correctness proof from it to IMM.

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 Article

  • 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), LIPIcs, Vol. 166, pp. 5:1 - 5:26, 2020. https://doi.org/10.4230/LIPIcs.ECOOP.2020.5
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