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
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.
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.
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.
An Algebraic Theory for Shared-State Concurrency dvir-2022-an
Algebraic foundations for effect-dependent optimisations kammar-2012-algebraic
Functorial Semantics of Algebraic Theories lawvere_1963
External (40)
- Effectful semantics in bicategories: strong, commutative, and concurrent pseudomonads (2024)
- Compositional Semantics for Shared-Variable Concurrency (2024)
- Denotational semantics of general store and polymorphism (2023)
- Retrofitting effect handlers onto OCaml (2021)
- On Thin Air Reads: Towards an Event Structures Model of Relaxed Memory (2019)
- Monads with merging (2019)
- Compositional Verification of Compiler Optimisations on Relaxed Memory (2018)
- Concurrent System Programming with Effect Handlers (2018)
- A Denotational Semantics for SPARC TSO (2018)
- Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics (2018)
- A monad for full ground reference cells (2017)
- Effect-dependent transformations for concurrent programs (2016)
- Programming with algebraic effects and handlers (2015)
- The Parallel Intensionally Fully Abstract Games Model of PCF (2015)
- Effective concurrency with algebraic effects (2015)
- Laws of Programming: The Algebraic Unification of Theories of Concurrency (2014)
- Local States in String Diagrams (2014)
- Algebraic theory of type-and-effect systems (2014)
- Handling Algebraic Effects (2013)
- Brookes is relaxed, almost! (2012)
- A separation logic for refining concurrent objects (2011)
- Some nuances of many-sorted universal algebra: A review (2011)
- Algebraic Theories: A Categorical Introduction to General Algebra (2010)
- A model of cooperative threads (2010)
- Handlers of Algebraic Effects (2009)
- Combining effects: Sum and tensor (2006)
- Discrete Lawvere theories and computational effects (2006)
- Some Varieties of Equational Logic (2006)
- Hennessy-Plotkin-Brookes revisited (2006)
- Algebraic Operations and Generic Effects (2003)
- Notions of Computation Determine Monads (2002)
- Possible world semantics for general storage in call-by-value (2002)
- The rely-guarantee method for verifying shared variable concurrent programs (1997)
- Full Abstraction for a Shared-Variable Parallel Language (1996)
- Domain Theory (1995)
- Notions of computation and monads (1991)
- A powerdomain for countable non-determinism (1982)
- Semantics of probabilistic programs (1981)
- Full abstraction for a simple parallel programming language (1979)
- Varieties of ordered algebras (1976)