  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.
