A Model of Cooperative Threads

摘要

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