A model of cooperative threads

DOI10.2168/LMCS-6(4:2)2010zbMATH Open1202.68105arXiv1009.2405OpenAlexW3102485161MaRDI QIDQ3064166FDOQ3064166

Gordon D. Plotkin, Martín Abadi

Publication date: 20 December 2010

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

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.

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

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

zbMATH Keywords

monaddenotational semanticstransactionoperational semantics

Mathematics Subject Classification ID

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

Cited In (4)

• Dynamic structural operational semantics
• Fair Cooperative Multithreading
• An algebraic theory for shared-state concurrency
• A comparison of concurrent programming and cooperative multithreading

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)