A Denotational Approach to Release/Acquire Concurrency

Extended Abstract Slides

Abstract: We want to report on recent and ongoing work into the denotational semantics of shared-state concurrent programming languages with Brookes-style trace semantics. Most of the talk would cover our trace semantics for the Release/Acquire (RA) memory model, a fragment of the C/C++ standard. Developing this semantics required us to re-think the interpretation of Brookes trace-sets, moving away from interrupted executions and towards a game-like/rely-guarantee-like intuition about the interaction of the program with its environment. We would like to present to the GALOP community these results and, time permitting, ongoing work about more general trace semantics for shared state, to facilitate discussion and further directions.