Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Ohad Kammar, Jack Liell-Cock, Sam Lindley, Cristina Matache, Sam Staton

TL;DR

The paper addresses the problem of giving a complete equational account of dynamic threads using algebraic effects, by formulating a parameterized algebraic theory for fork, wait, stop, and act_σ and proving representation and completeness theorems relative to labelled posets (pomsets). The main approach combines (i) a syntax-free representation of terms as labelled posets, (ii) a robust semantic model via strong monads on the functor category Set^{FinRel}, and (iii) a denotational framework that yields soundness, adequacy, and first-order full abstraction for the language. Key contributions include an eight-equation theory for the core concurrency primitives, a representation theorem showing an isomorphism between the term model and labelled poset model, and a completeness result ensuring open-term equations are captured by the pomset model; together with a denotational semantics that matches operational observations. The work advances the algebraic treatment of concurrency by treating thread IDs as abstract parameters, enabling modular reasoning about dynamic thread creation and binding, and offering a path to extending to richer concurrency features and effect handlers with principled compositional semantics.

Abstract

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.

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

TL;DR

The paper addresses the problem of giving a complete equational account of dynamic threads using algebraic effects, by formulating a parameterized algebraic theory for fork, wait, stop, and act_σ and proving representation and completeness theorems relative to labelled posets (pomsets). The main approach combines (i) a syntax-free representation of terms as labelled posets, (ii) a robust semantic model via strong monads on the functor category Set^{FinRel}, and (iii) a denotational framework that yields soundness, adequacy, and first-order full abstraction for the language. Key contributions include an eight-equation theory for the core concurrency primitives, a representation theorem showing an isomorphism between the term model and labelled poset model, and a completeness result ensuring open-term equations are captured by the pomset model; together with a denotational semantics that matches operational observations. The work advances the algebraic treatment of concurrency by treating thread IDs as abstract parameters, enabling modular reasoning about dynamic thread creation and binding, and offering a path to extending to richer concurrency features and effect handlers with principled compositional semantics.

Abstract

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.
Paper Structure (59 sections, 13 theorems, 60 equations, 9 figures)

This paper contains 59 sections, 13 theorems, 60 equations, 9 figures.

Table of Contents

  1. Introduction
  2. Contributions
  3. Motivating Fork and Wait with Thread IDs as Language Primitives
  4. A Simple Complete Fragment for Labelled Posets (Pomsets)
  5. Technical Setting: Functor Categories and Naturality for Syntax with Binding and Semantics with Names
  6. Fork and Wait in General, Parallel Composition, and Labelled Posets with Holes
  7. Paper Summary
  8. Background Concurrent Programming Language
  9. Language and Type System
  10. Operational Semantics
  11. Alternative Language Construct: $\mathsf{\underline{act}}_{\sigma}$
  12. Configurations
  13. Transition Relation
  14. Observation as a Labelled Poset
  15. Operational Meta-theory
  16. ...and 44 more sections

Key Result

proposition 1

Let $C_1=\langle w_1;\prec_1;\mathit{thread}_1\rangle$ and $C_2=\langle w_2;\prec_2;\mathit{thread}_2\rangle$. If $C_1$ is well-formed for $(A,<_1,w')$ and $C_1\xlongrightarrow{(\sigma)} C_2$ and $w'$ is disjoint from $w_2$, then there is a linear order $<_2$ extending $<_1$ such that $C_2$ is well-

Figures (9)

  • Figure 1: N-shape poset
  • Figure 2: Standard typing rules for a fine-grain call-by-value programming language. Here ${\mathbb{F}}$ is given in \ref{['eqn:fork-wait-geff-prims']}.
  • Figure 3: Operational semantics for our concurrent programming language (Sec. \ref{['sec:opsem']}). We write $\xlongrightarrow {(\sigma)}$ with parentheses to indicate two copies of the rule, one with the label and one without. Here $\mathit{tids}(a)=\{a\}$, $\mathit{tids}(v\oplus v')=\mathit{tids}(v)\cup \mathit{tids}(v')$, and $\mathit{tids}(\mathtt{0})=\emptyset$.
  • Figure 4: Graphical examples of terms built from the $\mathsf{node}$ operation. (a) is the term $\mathsf{node}_\tau(a_1,b.x(b,a_3))$; numbers $1$ and $2$ at the top correspond to the two inputs of variable $x:2$. (b) is the application of $\mathsf{node}_\sigma(a'_3, a_3.{-})$ to (a). (c) is the term in \ref{['eq:2']}; it is obtained from (b) by substituting $a_1 \oplus a_2$ for $a'_3$ as in \ref{['eq:3']}; (d) is obtained from (c) by substituting a term for the computation variable $x:2$, as in \ref{['eq:4']}.
  • Figure 5: Equations for the parameterized algebraic theory of dynamic threads $\mathcal{T}$.
  • ...and 4 more figures

Theorems & Definitions (30)

  • definition 1
  • definition 2
  • definition 3
  • definition 4
  • proposition 1: Preservation
  • proposition 2
  • definition 5
  • definition 6
  • definition 7
  • definition 8
  • ...and 20 more