LFCS Seminar: 28 April 2020 - Mark Batty
Title: Modular Relaxed Dependencies in Weak Memory Concurrency
Abtract:
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. We use this semantics to fix longstanding problems in the C++ memory model. We show that our C++ model is the first that avoids thin-air reads while aligning with the axiomatic-style specification of the ISO standard.
Affiliation:
University of Kent
Apr 28 2020
-
LFCS Seminar: 28 April 2020 - Mark Batty
Speaker: Mark Batty
Blackboard Collaborate:
https://eu.bbcollab.com/guest/dbb4b693c4b54e70bb3a07fb8cc5e9d7