Reference. A Brookes-Style Denotational Semantics for Release/Acquire Concurrency

We present a compositional denotational semantics for a functional language with first-class parallel composition and shared-memory 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 view-based machine for RA by Kang et al., 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.

Cite

Cite as @dvir-2025-a (helia, typst) · \cite{dvir-2025-a} (LaTeX)
BibTeX
bibtex · 1 line
@article{dvir-2025-a, title={A Brookes-Style Denotational Semantics for Release/Acquire Concurrency}, volume={47}, ISSN={1558-4593}, url={http://dx.doi.org/10.1145/3715096}, DOI={10.1145/3715096}, number={2}, journal={ACM Transactions on Programming Languages and Systems}, publisher={Association for Computing Machinery (ACM)}, author={Dvir, Yotam and Kammar, Ohad and Lahav, Ori}, year={2025}, month=May, pages={1–85} }
hayagriva YAML (typst)
yaml · 19 lines
dvir-2025-a:
  type: article
  title: A Brookes-Style Denotational Semantics for Release/Acquire Concurrency
  author:
  - Dvir, Yotam
  - Kammar, Ohad
  - Lahav, Ori
  date: 2025-05
  page-range: 1-85
  url: http://dx.doi.org/10.1145/3715096
  serial-number:
    doi: 10.1145/3715096
    issn: 1558-4593
  parent:
    type: periodical
    title: ACM Transactions on Programming Languages and Systems
    publisher: Association for Computing Machinery (ACM)
    issue: 2
    volume: 47
Cited by (1)

Two-sorted algebraic decompositions of Brookes’s shared-state denotational semantics dvir-2025-two

We define a two sorted equational theory of algebraic effects that models concurrent shared state with preemptive interleaving, recovering Brookes’s seminal 1996 trace-based model precisely. The decomposition allows us to analyse Brookes’s model algebraically in terms of separate but interacting components. The multiple sorts partition terms into layers. We use two sorts: a “hold” sort for layers that disallow interleaving of environment memory accesses, analogous to holding a global lock on the memory; and a “cede” sort for the opposite. The algebraic signature comprises of independent interlocking components: two new operators that switch between these sorts, delimiting the atomic layers, thought of as acquiring and releasing the global lock; non-deterministic choice; and state-accessing operators. The axioms similarly divide cleanly: the delimiters behave as a closure pair; all operators are strict, and distribute over non-empty non-deterministic choice; and non-deterministic global state obeys Plotkin and Power’s presentation of global state. Our representation theorem expresses the free algebras over a two-sorted family of variables as sets of traces with suitable closure conditions. When the held sort has no variables, we recover Brookes’s trace semantics. We define several other single-and two-sorted theories to elucidate the connection to Brookes’s model via translation embeddings and equivalences.
DOI · arXiv
Cites 53 works (2 here)
With notes (2)

A Denotational Approach to Release/Acquire Concurrency dvir-2024-a

We present a compositional denotational semantics for a functional language with first-class parallel composition and shared-memory 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.
PDF · DOI · pldb

An Algebraic Theory for Shared-State Concurrency dvir-2022-an

DOI · pldb
External (51)
dvir-2025-a reference entries/refs/dvir-2025-a/dvir-2025-a.hel