skip to content

Department of Computer Science and Technology

Thursday, 5 December, 2019 - 14:00 to 15:00
Marco Paviotti
Computer Laboratory, Room FW11

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 then use this semantics to fix the C++ memory model, which we call RD-C11 (Relaxed Dependencies C11). We show RD-C11 is the first C++ model the avoids thin-air reads that is aligned with the axiomatic-style specification of the ISO standard, provides the DRF-SC property, is efficiently implementable over hardware architectures and that is tested via a simulator over a battery of litmus tests.

Logic and Semantics Seminar (Computer Laboratory)

Upcoming seminars