LFCS Seminar: 28 April 2020 - Mark Batty
Title: Modular Relaxed Dependencies in Weak Memory Concurrency
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.
University of Kent