Reference. Two-sorted algebraic decompositions of Brookes’s shared-state denotational semantics

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.

Cite

Cite as @dvir-2025-two (helia, typst) · \cite{dvir-2025-two} (LaTeX)
BibTeX
bibtex · 1 line
@inbook{dvir-2025-two, title={Two-sorted algebraic decompositions of Brookes’s shared-state denotational semantics}, ISBN={9783031908972}, ISSN={1611-3349}, url={http://dx.doi.org/10.1007/978-3-031-90897-2_18}, DOI={10.1007/978-3-031-90897-2_18}, booktitle={Foundations of Software Science and Computation Structures}, publisher={Springer Nature Switzerland}, author={Dvir, Yotam and Kammar, Ohad and Lahav, Ori and Plotkin, Gordon}, year={2025}, pages={377–398} }
hayagriva YAML (typst)
yaml · 19 lines
dvir-2025-two:
  type: chapter
  title: Two-sorted algebraic decompositions of Brookes’s shared-state denotational semantics
  author:
  - Dvir, Yotam
  - Kammar, Ohad
  - Lahav, Ori
  - Plotkin, Gordon
  date: 2025
  page-range: 377-398
  url: http://dx.doi.org/10.1007/978-3-031-90897-2_18
  serial-number:
    doi: 10.1007/978-3-031-90897-2_18
    isbn: '9783031908972'
    issn: 1611-3349
  parent:
    type: book
    title: Foundations of Software Science and Computation Structures
    publisher: Springer Nature Switzerland
Cited by (1)

An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on Finite Relations, Labelled Posets, and Parameterized Algebraic Theories kammar-2026-an

We use the theory of algebraic effects to give a complete equational axiomatization for dynamic threads. Our method is based on parameterized algebraic theories, which give a concrete syntax for strong monads on functor categories, and are a convenient framework for names and binding. Our programs are built from the key primitives ‘fork’ and ‘wait’. ‘Fork’ creates a child thread and passes its name (thread ID) to the parent thread. ‘Wait’ allows us to wait for given child threads to finish. We provide a parameterized algebraic theory built from fork and wait, together with basic atomic actions and laws such as associativity of ‘fork’. Our equational axiomatization is complete in two senses. First, for closed expressions, it completely captures equality of labelled posets (pomsets), an established model of concurrency: model complete. Second, any two open expressions are provably equal if they are equal under all closing substitutions: syntactically complete. The benefit of algebraic effects is that the semantic analysis can focus on the algebraic operations of fork and wait. We then extend the analysis to a simple concurrent programming language by giving operational and denotational semantics. The denotational semantics is built using the methods of parameterized algebraic theories and we show that it is sound, adequate, and fully abstract at first order for labelled-poset observations.
DOI · arXiv · pldb
Cites 45 works (5 here)
With notes (5)

A Brookes-Style Denotational Semantics for Release/Acquire Concurrency dvir-2025-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 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.
DOI · pldb

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

Algebraic foundations for effect-dependent optimisations kammar-2012-algebraic

PDF · DOI · pldb

Functorial Semantics of Algebraic Theories lawvere_1963

Web
External (40)
dvir-2025-two reference entries/refs/dvir-2025-two/dvir-2025-two.hel