A Denotational Approach to Release/Acquire Concurrency

Yotam Dvir, Ohad Kammar, Ori Lahav

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

We present a compositional denotational semantics for a functional language with first-class parallel composition and shared-mem- ory operations whose operational semantics follows the Release/Acquire weak memory model (RA). The semantics is formulated in Moggi’s monadic approach, and is based on Brookes-style traces. To do so we adapt Brookes’s traces to Kang et al.’s view-based machine for RA, and supplement Brookes’s mumble and stutter closure operations with additional operations, specific to RA. The latter provides a more nuanced understanding of traces that uncouples them from operational interrupted executions. We show that our denotational semantics is adequate and use it to validate various program transformations of interest. This is the first work to put weak memory models on the same footing as many other programming effects in Moggi’s standard monadic approach.
Original languageEnglish
Title of host publicationProceedings from the European Symposium on Programming (ESOP)
Number of pages27
Publication statusAccepted/In press - 19 Jan 2024
Event33rd European Symposium on Programming - Luxembourg City, Luxembourg
Duration: 6 Apr 202411 Apr 2024
Conference number: 33

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
ISSN (Print)0302-9743


Conference33rd European Symposium on Programming
Abbreviated titleESOP 2024
CityLuxembourg City


Dive into the research topics of 'A Denotational Approach to Release/Acquire Concurrency'. Together they form a unique fingerprint.

Cite this