Skip to main content

Modular Relaxed Dependencies in Weak Memory Concurrency

Paviotti, Marco, Cooksey, Simon, Paradis, Anouk, Wright, Daniel, Owens, Scott, Batty, Mark (2020) Modular Relaxed Dependencies in Weak Memory Concurrency. In: Lecture Notes in Computer Science. Programming Languages and System: 29th European Symposium on Programming, ESOP 2020 Held as Part of the European Joint Conferences on Theory and Practice of Software. 12075. pp. 599-625. Springer ISBN 978-3-030-44913-1. (doi:10.1007/978-3-030-44914-8_22) (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided) (KAR id:81430)

The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided. (Contact us about this Publication)
Official URL
https://doi.org/10.1007/978-3-030-44914-8_22

Abstract

We present a denotational semantics for weak memory concurrency that avoids thin-air reads, provides data-race free programs with sequentially consistent semantics (DRF-SC), and supports a compositional refinement relation for validating optimisations. Our semantics identifies false program dependencies that might be removed by compiler optimisation, and leaves in place just the dependencies necessary to rule out thin-air reads. We show that our dependency calculation can be used to rule out thin-air reads in any axiomatic concurrency model, in particular C++. We present a tool that automatically evaluates litmus tests, show that we can augment C++ to fix the thin-air problem, and we prove that our augmentation is compatible with the previously used compilation mappings over key processor architectures. We argue that our dependency calculation offers a practical route to fixing the longstanding problem of thin-air reads in the C++ specification.

Item Type: Conference or workshop item (Proceeding)
DOI/Identification number: 10.1007/978-3-030-44914-8_22
Uncontrolled keywords: Thin-air problem, Weak memory concurrency, Compiler Optimisations, Denotational Semantics, Compositionality
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 75 Electronic computers. Computer science
Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Batty
Date Deposited: 28 May 2020 13:58 UTC
Last Modified: 16 Feb 2021 14:13 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/81430 (The current URI for this page, for reference purposes)
Owens, Scott: https://orcid.org/0000-0002-7437-4780
Batty, Mark: https://orcid.org/0000-0001-7053-4364
  • Depositors only (login required):