Document Open Access Logo

Brief Announcement: Generalising Concurrent Correctness to Weak Memory

Authors Simon Doherty, Brijesh Dongol, Heike Wehrheim, John Derrick

PDF
Thumbnail PDF

File

LIPIcs.DISC.2018.45.pdf
  • Filesize: 377 kB
  • 3 pages

Document Identifiers

Author Details

Simon Doherty
  • Department of Computer Science, University of Sheffield, UK
Brijesh Dongol
  • Department of Computer Science, University of Surrey, Guildford, UK
Heike Wehrheim
  • Department of Computer Science, Paderborn University, Paderborn, Germany
John Derrick
  • Department of Computer Science, University of Sheffield, UK

Funding

  • Doherty, Simon: Simon Doherty and John Derrick are funded by EPSRC Grant EP/M017044/1.
  • Dongol, Brijesh: Funded by EPSRC Grant EP/R019045/1.

Cite AsGet BibTex

Simon Doherty, Brijesh Dongol, Heike Wehrheim, and John Derrick. Brief Announcement: Generalising Concurrent Correctness to Weak Memory. In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, pp. 45:1-45:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.DISC.2018.45

Abstract

Correctness conditions like linearizability and opacity describe some form of atomicity imposed on concurrent objects. In this paper, we propose a correctness condition (called causal atomicity) for concurrent objects executing in a weak memory model, where the histories of the objects in question are partially ordered. We establish compositionality and abstraction results for causal atomicity and develop an associated refinement-based proof technique.

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Theory of computation → Shared memory algorithms
Keywords
  • Weak Memory
  • Concurrent Object
  • Execution Structure

Metrics

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

References

  1. S. Doherty, B. Dongol, H. Wehrheim, and J. Derrick. Making Linearizability Compositional for Partially Ordered Executions. In iFM, volume 11023 of LNCS, 2018. Google Scholar
  2. S. Doherty, L. Groves, V. Luchangco, and M. Moir. Towards formally specifying and verifying transactional memory. Formal Asp. Comput., 25(5):769-799, 2013. Google Scholar
  3. A. Farzan and P. Madhusudan. Causal atomicity. In CAV, volume 4144 of LNCS, pages 315-328. Springer, 2006. Google Scholar
  4. L. Lamport. On interprocess communication. part I: basic formalism. Distributed Computing, 1(2):77-85, 1986. Google Scholar
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