A Model of Cooperative Threads

TL;DR

This paper introduces a trace-based denotational semantics for a small imperative language with cooperative threads, providing a fully abstract mathematical model and an equational theory for computational effects like thread spawning.

Contribution

It presents a novel, fully abstract semantics for cooperative threads and develops an algebraic framework for understanding their computational effects.

Findings

Semantics is fully abstract and mathematically elementary.

Provides an equational theory for thread spawning effects.

Analyzes threads using the free algebra monad.

Abstract

We develop a model of concurrent imperative programming with threads. We focus on a small imperative language with cooperative threads which execute without interruption until they terminate or explicitly yield control. We define and study a trace-based denotational semantics for this language; this semantics is fully abstract but mathematically elementary. We also give an equational theory for the computational effects that underlie the language, including thread spawning. We then analyze threads in terms of the free algebra monad for this theory.