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

We decompose Brooke’s pioneering denotational model of concurrent shared state under preemptive interleaving [6] using algebraic effects [30]. This model possesses several desirable features in the area of denotational models for programming languages with concurrent features. (I) It is based on traces, an elementary sequential gadget. (II) It is fully compositional, as in traditional denotational semantics for shared-state [e.g. 15, 17]. Each syntactic programming construct, including parallel composition, has a corresponding semantic operation combining the meanings of its constituents. Such full compositionality contrasts with some recent models in this area that require additional ‘semantic post-processing’: some form of quotient, pruning of auxiliary mathematical constructs, reasoning up/to behavioural equivalence; or capture only sequential blocks, reasoning about the parallel composition on a separate layer [e.g. 7, 8, 19, 21]. (III) Subsequent variations and extensions [4, 38, 39], as well as adaptations to relaxed memory models [12, 13, 21], attest to its versatility, making it a cornerstone in the denotational semantics for concurrent languages with side-effects. (IV) It achieves a high level of abstraction, evident in the many compiler transformations that the model supports, including the most common memory access introductions and eliminations, and the laws of parallel programming. Moreover, Brookes showed the model to be fully abstract in a language extended with the await construct, which blocks execution until all memory locations contain a given tuple of values, and then atomically updates them to contain another tuple of values. This construct is not a natural programming construct, but is clearly suggested by Brookes’s semantics.

Plotkin and Power’s modern theory of algebraic effects [30] refines Moggi’s monadic approach [26] with algebraic theories. The algebraic approach informs the monadic structure by identifying semantic counterparts to syntactic constructs and axiomatising their semantics equationally. The monadic structure emerges through the well-established connection between algebraic theories and monads [23] via representation theorems. For example: global state emerges by axiomatising memory lookup and update [30] and a representation theorem involving the state monad; non-determinism emerges by axiomatising semi-lattices and a representation theorem involving the powerdomains [15, 28]; and so on. The algebraic perspective may offer insights into the making of the denotational semantics. It can suggest methods for combining different effects and modularly augment a semantics with a given computational effect [17].

The connection between algebraic effects and concurrency has long been emphasised. For example, the ability to use algebraic effects, without any axioms, and their effect handlers [3, 32, 33] to allow users to define their own schedulers was the original motivation for their implementation in the OCaml programming language [9, 10, 35]. Nonetheless, exhibiting abstract models such as Brookes’s algebraically via equational axiomatisation of syntactic constructs has proved challenging. Our own previous algebraic model [11] invalidates a key transformation, reflecting a fundamental limitation.

To overcome this limitation, we use multi-sorted algebraic theories, a direction that was raised in personal discussions since the earliest work on algebraic effects [30]. A multi-sorted algebraic term decomposes into layers. Our two sorts represent two modes of interaction between a program fragment and its concurrent environment. A “hold” sort (\(\bullet \)) provides a reasoning layer in which the environment may not interfere, whereas in the “cede” sort ( ) it may. We provide two operators that switch between these sorts. Our core idea is to axiomatise these operators as a closure pair, an established order-theoretic special Galois-connection, the dual to the domain-theoretic embedding-projection pairs [1]. Additionally, we axiomatise strict distributivity of the closure pair over non-determinism. The remaining axioms, all in the hold sort, are strikingly independent from these axioms. In our shared-state theory , the remaining axioms are precisely those of non-deterministic global state.

We prove, twice over, that recovers Brookes’s model in the cede sort. First, using sets of traces akin to Brookes’s, we define a representation of . The representation recovers Brookes’s model via the adjunction that forgets the hold sort. Second, we define three algebraic theories for Brookes’s await and its sequential variant, relating them to global-state, shared-state, and each other via embeddings and equivalences. The theory for concurrent await is straightforwardly represented by Brookes’s model, and embeds in the cede sort of .

Caveats In our development, we opt for mathematical simplicity whenever possible. For example, we use countable-join semilattices instead of finite-join semilattices to represent non-determinism. This choice streamlines the development leading up to the representation theorem, allowing us to use countable sets instead of finitely generated ones. We also do not treat recursion to avoid the complexity that a domain-theoretic account incurs. The resulting model—identical to Brookes’s—coincides with the elided domain-theoretic model over discrete pre-domains. This model also supports iteration (i.e. while-loops) without change thanks to countable-joins. It also supports first-order recursion without change by equipping it with a domain-theoretic structure. These compromises let us focus on the core concepts, and provide a relatively elementary exposition and a clear presentation of the underlying idea, motivating future inquiry.

Equational theories study terms constructed from algebraic operators (§3.1). In Plotkin and Power’s algebraic theory of effects, the operators represent fundamental program effects, and their arguments represent continuations. Equational axioms reflect fundamental relationships between the operators. The equations that hold in the theory, reflecting the semantics as a whole, are those that follow from its axiomatic presentation by equational logic (§3.2).

In the global-state theory, a theory for sequential stateful computation, the operators and represent updating and looking up bits in memory. For example, consider the global-state term . After updating \(\texttt {y}\) to \(0\), the computation looks \(\texttt {y}\) up: if it finds \(0\), it returns 3; if it finds \(1\), it updates \(\texttt {x}\) and \(\texttt {y}\) to \(1\) in succession, then returns 7. Between the update and the lookup, the value at \(\texttt {y}\) cannot change. Therefore, the computation finds the value \(0\), and takes the left-hand continuation. The global-state axiom () reflects this fact. By (), \({\textsf {U}}_{\texttt {y},0}{\textsf {L}}_{\texttt {y}}( 3,{\textsf {U}}_{\texttt {x},1}{\textsf {U}}_{\texttt {y},1}7 ) = {\textsf {U}}_{\texttt {y},0} 3\) holds in global state.

A representing monadic model for an equational theory (§3.3) interprets the algebraic operators as corresponding operations over the model’s domain; such that each term, up-to equality in the theory, is represented uniquely in the domain. Interpretations respect the theory; that is, applying an operation to representations of terms results in the representation of the corresponding operator applied to said terms: . For example, global-state terms are represented by memory-manipulating functions in the state-monad model. This model interprets update by precomposing a state update ; and interprets lookup by passing the input memory state along to the -continuation . In this way, global state recovers the (historically precedent) state monad.

The state monad does not account for concurrent interference. The monad underlying Brookes’s denotational semantics does, by using sequences of transitions to denote potential behaviours (§6.1). Each transition in sequence means that the computation, by relying on exclusive access to the memory at state , can guarantee to provide the state and yield to the environment.

Following the tradition of algebraic effects, we wish to recover Brookes’s model using an equational theory for shared state. This is rather straightforward using a single-sorted theory \(\textsf {B}\) (§6.3) in which transitions appear as operators. However, this theory is dissatisfying, for two reasons. (I) Transitions do not correspond to familiar programming constructs, but to Brookes artificial await construct. (II) Conceptualising shared state as global state with concurrent interference, we expect the global-state effects to be present in a theory of shared state, and the equations between them to hold when interference is prohibited.

A more appropriate approach adds an operator \({\textsf {Y}}\) to global state for yielding control to the environment. Otherwise, the computation has exclusive access to memory. This direction lead to a Brookes-like model [11]. However, unlike Brookes’s model, it does not validate the Irrelevant Read Introduction (IRI) program transformation, which introduces a read instruction that possibly yields to the environment and discards the value it read. The IRI transformation is useful as a stepping stone to other practical transformations, such as common-subexpression elimination from conditionals, and consequently loops. Invalidating IRI seems to be a fundamental limitation of the yield-operator approach, as we show in the extended manuscript [14, §A]. In retrospect, we can pinpoint the issue to \({\textsf {Y}}\) both releasing exclusive access to memory, and acquiring it back. Our key insight is that the mode of computation that cedes access to memory needs to be explicit, decomposing \({\textsf {Y}}\) into a pair of mode-switching operators.

The remaining structure falls into place straightforwardly and naturally, in our proposed two-sorted theory for shared state (§4). Each sort represents a computation mode: hold \((\bullet )\) represents the computation’s exclusive access to memory; cede represents positions in which the environment may interfere. Each operator has a sort and expects each continuation to have a specific sort. In , update and lookup are -sorted continuations, allowing us to reason about interference-free stateful interactions.

The theory also supports non-deterministic choice in both sorts. For example, the term either updates \(\texttt {x}\) to \(1\) and returns 2, or updates \(\texttt {x}\) to \(1\) and returns 5. We axiomatise such that each operator distributes over non-deterministic choice, e.g. . We order terms by potential behaviours \((l \ge r) :==(l = l \vee r)\), a partial-order for -equality (§3.2).

The mode-switching operators of are and . That is, \(\mathop {\lhd }\) is -sorted and expects a \(\bullet \)-sorted continuation, and vice versa for \(\mathop {\rhd }\). We think of them as delimiting atomic blocks, or acquiring and releasing an abstract global lock. We axiomatise them in by strict distributivity over countable joins, i.e. () and () ; and:

These axiomatise \(\mathop {\lhd }\) and \(\mathop {\rhd }\) as an (insertion)-closure pair [e.g. 1].

Each -term denotes a set of sort-delimited traces (§5.1), which generalise Brookes’s traces. For example, \(t:=={\textsf {U}}_{\texttt {y},0}\mathop {\rhd }\mathop {\lhd }{\textsf {L}}_{\texttt {y}}( 3,{\textsf {U}}_{\texttt {x},1}{\textsf {U}}_{\texttt {y},1}\mathop {\rhd }7 )\) denotes a set that includes . Indeed, we can read off a corresponding computation from \(t\), initially holding the lock in the state \(\left( {\begin{smallmatrix}\texttt {x}\mapsto 1 \\ \texttt {y}\mapsto 1 \end{smallmatrix}}\right) \) of both bits \(1\): the computation updates \(\texttt {y}\) to \(0\), then yields to the environment before looking \(\texttt {y}\) up; finding \(1\), it updates \(\texttt {x}\) and \(\texttt {y}\) to \(1\), then releases the lock and returns 7. Brookes’s original traces correspond to those delimited by on both ends.

With these traces we define our two-sorted generalisation of Brookes’s model, and prove that it represents (§5.2). The -sorted -valued fragment (§6.2), which represents the “block-closed” terms, is Brookes’s original model (§6.1).

We also provide an algebraic perspective on the representation, by -embedding (§6.4) the transitions-theory \(\textsf {B}\) into (§6.5). This embedding maps to , where is defined by global-state operators (§5.2).

We present a standard treatment of countably-infinitary multi-sorted equational theories and their free models [e.g. 2, 37], straightforwardly generalising the single-sorted case by assigning sorts to functions and their arguments. The reader may choose to skim/skip this section, consulting it as necessary.

To define the equational theory of shared state, we first recall the standard, single sorted (non-deterministic) global state theory \(\textsf {G}\) [17, 25, 30]. The variant we present here has countable non-determinism, and the global state operators manipulate a common memory store with a finite set of locations each storing a bit . A larger finite set of storable-values would not be conceptually different. Infinite sets of storable-values or locations work similarly with more involved representation theorems. In concrete examples, we let and use non-bracketed vectors for stores, e.g. denotes .

The signature \(\Sigma _{\textsf {G}}\) consists of the countable-join semilattice operators (example 2), as well as two kinds of memory-access operators: lookup operators \({\textsf {L}}_{\ell } : 2\), to look a location up and branch according to the value found; and update operators \({\textsf {U}}_{\ell ,b} : 1\), to update a location \(\ell \in \mathbb {L}\) to the value . The global state axioms consists of the countable-join semilattice axioms (example 5), as well as the following:

The induced algebraic theory \(\textsf {G}\) includes axioms of less succinct presentations of the same theory [25]. For example, lookup also distributes over binary join, so the theory admits inequational reasoning; consecutively looking the same location up can be merged, e.g. ; and other combinations of looking-up and updating different locations commute, e.g. for any we have .

Our two-sorted presentation of shared state extends global state. Its sorts are . The hold sort \((\bullet )\) represents an uninterrupted sequence of memory accesses, whereas the cede sort allows control to pass to the environment. The operators and the arities of the signature consist of a copy of \(\Sigma _{\textsf {G}}\) at \(\bullet \), a copy of at , and new operators and .

The intuitive reading for algebraic effects is from the outside in. With this intuition, one interpretation of the operators \(\mathop {\lhd }\) and \(\mathop {\rhd }\) is to acquire and release a global lock. The hold sort (\(\bullet \)) represents the lock being held by one of the threads in the program. The cede sort ( ) represents points in the execution in which one of the threads in the concurrent environment may acquire the lock. The sorts ensure exclusive access to the lock, and therefore to the store. In an alternative interpretation, these operators delimit atomic blocks; their sorts prevent nesting.

The shared state axioms include a copy of the (non-deterministic) global state axioms at \(\bullet \) and a copy of the countable-join semilattice axioms \(\text {Ax}_{\textsf {V}}\) at . In particular, proves the semi-lattice axioms in both sorts. It further includes standard strict distributivity axioms for the new unary operators:

With these axioms, supports inequational reasoning, which represents the semantic refinement relation used to validate program transformations [e.g. 11].

Finally, axiomatises \(\mathop {\lhd }\) and \(\mathop {\rhd }\) as an (insertion)-closure pair [e.g. 1]:

They are compatible with the global-lock interpretation:

To summerise, .

We now establish the representation theorem describing a free -model over any . Following Brookes [6], we use sets of traces to denote behaviours.

The theory recovers Brookes’s model (§6.1). We recover it twice, using different strategies that offer different perspectives. The first transforms the monad induced by the representation of §5.2 along a right adjoint sending each -family to the set (§6.2). In the second, we define a single-sorted theory of transitions \(\textsf {B}\) that recovers Brookes’s model straightforwardly (§6.3). In this theory, the transition operators correspond to Brookes’s await construct. After swiftly introducing embedding translations (§6.4), we show that \(\textsf {B}\) embeds into . The embedding factors through another, two-sorted, theory of transitions \(\textsf {T\!r}\) (§6.5).

We presented an equational theory for shared state ( ). It separates reasoning into two layers. In the held layer (\(\bullet \)), we prohibit the concurrent environment from accessing memory, and we can reason about memory accesses by a pool of threads sequentially. In the ceded layer ( ), the concurrent environment may interleave, and local memory access is forbidden. We also presented theories of transitions (\(\textsf {B}\), \(\textsf {T\!gs}\), & \(\textsf {T\!r}\)) and formally related them to (non-deterministic) global state (\(\textsf {G}\)) and shared state ( ). The single-sorted theory \(\textsf {B}\) recovers Brookes’s model, but it does so by using Brookes’s await construct, which we find unnatural; and it does not admit global state explicitly as a component of the theory. We believe that admitting global state will inform modelling other effects in the concurrent setting. Our theory addresses these concerns. It admits the global state theory as-is, and axiomatises the mode-switching operators ( /\(\mathop {\rhd }\)) without explicit interaction with global state. This theory recovers Brookes’s model exactly, in a principled manner: by transforming a monad and its operations along an adjunction; and, independently, through algebraic translations.

Our theory uses countable-join semilattices to recover Brookes’s model. They can express iteration (i.e. while-loops). The same model admits first-order recursion, i.e. least-fixpoints of mutually-defined first-order functions, using the \(\omega \)-complete partial order structure of the refinement order and the Scott-continuity of the semantics. We can support higher-order recursion by recourse to domain-theory, generalising algebraic theories using order-enriched theories. There are several standard variants, each with subtle logical trade-offs [29]. We can also restrict the semantics to terminating languages by restricting to finite joins, and using finitely-generated closed subsets for the representation.

We want to analyse Brookes’s parallel composition operator algebraically. Brookes composed programs in parallel by interleaving traces from each thread. Initial results show we can define Brookes’s parallel composition by simultaneous induction over terms. However, we would like to provide a more abstract account, by recourse to the universal property of free models. This abstraction may expose special properties of global state, or lead to a general parallel composition operation satisfying the expected laws of concurrent programming [16, 27, 34].

We would like to model more effects within this modular multi-sorted algebraic framework. These effects include: more advanced notions of state, such as dynamic allocation [20], higher-order memory cells [24, 36], and weak memory [12, 13]; control-flow effects such as exceptions and effect handlers [3]; and probabilistic programming with shared state [22].

If the multi-sorted approach does indeed generalise to more sophisticated effects, then it will be instructive to review its assumptions. For example, the strictness axioms impose a partial-correctness discipline: the semantics says nothing about the effect a diverging program has on its memory. Relaxing or removing strictness may give a model that allows us to reason about diverging programs.

Our two sorts limit access to the whole store. We would like to explore finer granularity. For example, a theory with per-location access limitation, with sorts for every finite subset \(s \subseteq \mathbb {L}\) of locations, and operators and . We expect the axiomatisation’s design to require subtlety.

It may be interesting to to expose the sort discipline in the surface language through typing judgements, explicating regions that rule out data-races with the environment. It seems such judgements would rule out deadlocks structurally, and so may limit expressiveness. Whether this idea is useful remains to be seen.

In conclusion, our two-sorted decomposition of Brookes’s seminal model provides new insights into its assumptions and components, and reveals new directions for modelling more advanced features involving concurrent shared state.