Two-sorted algebraic decompositions of Brookes's shared-state denotational semantics

TL;DR

This paper introduces a two-sorted algebraic framework to model and analyze Brookes's shared-state semantics for concurrent programs, enabling algebraic decomposition and precise trace-based representation.

Contribution

It presents a novel two-sorted algebraic theory that decomposes Brookes's model into interacting components, facilitating algebraic analysis of shared-state concurrency.

Findings

Recover Brookes's trace semantics as a special case

Decompose shared-state model into algebraic components

Provide a representation theorem for free algebras

Abstract

We use a two sorted equational theory of algebraic effects to model 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.