A model of cooperative threads

DOI10.2168/LMCS-6(4:2)2010MaRDI QIDQ3064166zbMATH OpenOpenAlexFDO

Authors Martín Abadi, Gordon D. Plotkin

Publication date 20 December 2010

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1009.2405

zbMATH Keywords

denotational semanticsmonadoperational semanticstransaction

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

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.

Recommendations

• A model of cooperative threads
• Fair Cooperative Multithreading
• Towards a semantic theory of CML
• Synchronous cooperation for explicit multi-threading
• Denotational semantics for thread algebra

Cited in

(10)

• Safe-for-space threads in standard ML
• Dynamic structural operational semantics
• Trampolined style
• Compiling cooperative task management to continuations
• Fair Cooperative Multithreading
• A comparison of concurrent programming and cooperative multithreading
• A model of cooperative threads
• An algebraic theory for shared-state concurrency
• Asynchronous Cooperative Contracts for Cooperative Scheduling
• Choice trees: representing and reasoning about nondeterministic, recursive, and impure programs in Rocq

This page was built for publication: A model of cooperative threads

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3064166)