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 16.00 - 17.00 LFCS Seminar: 28 April 2020 - Mark Batty Speaker: Mark Batty Blackboard Collaborate: https://eu.bbcollab.com/guest/dbb4b693c4b54e70bb3a07fb8cc5e9d7
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 16.00 - 17.00 LFCS Seminar: 28 April 2020 - Mark Batty Speaker: Mark Batty Blackboard Collaborate: https://eu.bbcollab.com/guest/dbb4b693c4b54e70bb3a07fb8cc5e9d7
