About: Modular Relaxed Dependencies in Weak Memory Concurrency

Not logged in : Login

(Sponging disallowed)

Facets (new session)
Description
Metadata
Settings
- Rule:
- Inverse Functional Properties:
- "Same As":

About: Modular Relaxed Dependencies in Weak Memory Concurrency Goto Sponge Distinct Permalink

An Entity of Type : bibo:AcademicArticle, within Data Space : linkeddata.uriburner.com:28898 associated with source document(s)

Attributes	Values
type	http://eprints.org/ontology/ConferenceItemEPrint http://eprints.org/ontology/ConferenceItemEPrint http://eprints.org/ontology/EPrint http://eprints.org/ontology/EPrint Article Article Academic Article Academic Article
seeAlso	HTML Summary of #81430 Modular Relaxed Dependencies in Weak Memory Concurrency HTML Summary of #81430 Modular Relaxed Dependencies in Weak Memory Concurrency
sameAs	Modular Relaxed Dependencies in Weak Memory Concurrency Modular Relaxed Dependencies in Weak Memory Concurrency
Title	Modular Relaxed Dependencies in Weak Memory Concurrency Modular Relaxed Dependencies in Weak Memory Concurrency
described by	https://demo.openlinksw.com/about/id/entity/https/www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/export_kar_RDFN3.n3 https://demo.openlinksw.com/about/id/entity/https/raw.githubusercontent.com/annajordanous/CO644Files/main/export_kar_RDFN3.n3
Date	2020 2020
Creator	Marco Paviotti Marco Paviotti Anouk Paradis Anouk Paradis Simon Cooksey Simon Cooksey Daniel Wright Daniel Wright Mark Batty Mark Batty Scott Owens Scott Owens
status	peer reviewed peer reviewed published published
Publisher	Springer Springer
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. 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.
Is Part Of	Financial Cryptography and Data Security Financial Cryptography and Data Security https://kar.kent.ac.uk/id/repository https://kar.kent.ac.uk/id/repository
Subject	QA 75 Electronic computers. Computer science QA 75 Electronic computers. Computer science QA 76 Software, computer programming, QA 76 Software, computer programming,
list of authors	https://kar.kent.ac.uk/id/eprint/81430#authors https://kar.kent.ac.uk/id/eprint/81430#authors
presented at	29th European Symposium on Programming, ESOP 2020 29th European Symposium on Programming, ESOP 2020
volume	12075 12075
is topic of	https://www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/export_kar_RDFN3.n3 https://raw.githubusercontent.com/annajordanous/CO644Files/main/export_kar_RDFN3.n3
is primary topic of	HTML Summary of #81430 Modular Relaxed Dependencies in Weak Memory Concurrency HTML Summary of #81430 Modular Relaxed Dependencies in Weak Memory Concurrency

Faceted Search & Find service v1.17_git144 as of Jul 26 2024

Alternative Linked Data Documents: iSPARQL | ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 08.03.3331 as of Aug 25 2024, on Linux (x86_64-ubuntu_noble-linux-glibc2.38-64), Single-Server Edition (378 GB total memory, 37 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software