Modular Relaxed Dependencies in Weak Memory Concurrency
- đ¤ Speaker: Marco Paviotti đ Website
- đ Date & Time: Thursday 05 December 2019, 14:00 - 15:00
- đ Venue: Computer Laboratory, Room FW11
Abstract
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.
Series This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.
Included in Lists
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- Computer Laboratory, Room FW11
- Computing and Mathematics
- Department of Computer Science and Technology talks and seminars
- Interested Talks
- Logic and Semantics Seminar (Computer Laboratory)
- Martin's interesting talks
- School of Technology
- tcw57âs list
- Trust & Technology Initiative - interesting events
- yk373's list
- yk449
Note: Ex-directory lists are not shown.
![[Talks.cam]](/static/images/talkslogosmall.gif)



Thursday 05 December 2019, 14:00-15:00