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
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.
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.
An Algebraic Theory for Shared-State Concurrency dvir-2022-an
External (51)
- Compositional Semantics for Shared-Variable Concurrency (2024)
- Weakest preconditions in fibrations (2022)
- The leaky semicolon: compositional semantic dependencies for relaxed-memory concurrency (2022)
- Sequential reasoning for optimizing compilers under weak memory concurrency (2022)
- Making weak memory models fair (2021)
- Modular data-race-freedom guarantees in the promising semantics (2021)
- Pomsets with preconditions: a simple model of relaxed memory (2020)
- Modular Relaxed Dependencies in Weak Memory Concurrency (2020)
- Verification under causally consistent shared memory (2019)
- The next 700 relational program logics (2019)
- An introduction to logical relations (2019)
- A Denotational Semantics for SPARC TSO (2018)
- Compositional Verification of Compiler Optimisations on Relaxed Memory (2018)
- Repairing sequential consistency in C/C++11 (2017)
- A promising semantics for relaxed-memory concurrency (2017)
- Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8 (2017)
- Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (2017)
- Formalizing and Checking Thread Refinement for Data-Race-Free Execution Models (2016)
- Taming release-acquire consistency (2016)
- Explaining Relaxed Memory Models with Program Transformations (2016)
- Validating optimizations of concurrent C/C++ programs (2016)
- Effect-dependent transformations for concurrent programs (2016)
- Weak memory models using event structures (2016)
- The Problem of Programming Language Concurrency Semantics (2015)
- Common compiler optimisations are invalid in the C11 memory model and what we can do about it (2015)
- The laws of programming unify process calculi (2014)
- Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations (2014)
- Abstract effects and proof-relevant logical relations (2014)
- Compiler testing via a theory of sound optimisations in the C11/C++11 memory model (2013)
- Brookes Is Relaxed, Almost! (2012)
- A rely-guarantee-based simulation for verifying concurrent program transformations (2012)
- A Concurrent Logical Relation (2012)
- Mathematizing C++ concurrency (2011)
- Understanding POWER multiprocessors (2011)
- A separation logic for refining concurrent objects (2011)
- A Model of Cooperative Threads (2010)
- Verifying Local Transformations on Relaxed Memory Models (2010)
- A Better x86 Memory Model: x86-TSO (2009)
- Relational semantics for effect-based program transformations: higher-order store (2009)
- Correctness of effect-based program transformations (2008)
- A semantics for concurrent separation logic (2007)
- Relational semantics for effect-based program transformations with dynamic allocation (2007)
- Relational reasoning in a nominal semantics for storage (2005)
- The Java memory model (2005)
- Monads and effects (2002)
- Notions of computation determine monads (2002)
- The rely-guarantee method for verifying shared variable concurrent programs (1997)
- Full Abstraction for a Shared-Variable Parallel Language (1996)
- Notions of computation and monads (1991)
- How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs (1979)
- Lambda-Definability and Logical Relations (1973)