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: | 21 Dec 2022 20:49 UTC |
| Resource URI: | https://kar.kent.ac.uk/id/eprint/81430 (The current URI for this page, for reference purposes) |
University of Kent Author Information
Paviotti, Marco.
| Creator's ORCID: |
 https://orcid.org/0000-0002-1513-0807
|
|---|---|
| CReDIT Contributor Roles: |
Owens, Scott.
| Creator's ORCID: |
https://orcid.org/0000-0002-7437-4780
|
|---|---|
| CReDIT Contributor Roles: |
Batty, Mark.
| Creator's ORCID: |
https://orcid.org/0000-0001-7053-4364
|
|---|---|
| CReDIT Contributor Roles: |
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):
Altmetric
Altmetric
