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