{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:27:53Z","timestamp":1767929273240,"version":"3.49.0"},"reference-count":36,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2010,10,20]],"date-time":"2010-10-20T00:00:00Z","timestamp":1287532800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.2168\/lmcs-6(4:2)2010","type":"journal-article","created":{"date-parts":[[2010,11,26]],"date-time":"2010-11-26T21:56:28Z","timestamp":1290808588000},"source":"Crossref","is-referenced-by-count":7,"title":["A Model of Cooperative Threads"],"prefix":"10.46298","volume":"Volume 6, Issue 4","author":[{"given":"Mart\u00edn","family":"Abadi","sequence":"first","affiliation":[]},{"given":"Gordon D.","family":"Plotkin","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2010,10,20]]},"reference":[{"key":"10.2168\/LMCS-6(4:2)2010_abadi:semantics","doi-asserted-by":"crossref","unstructured":"Mart\u00edn Abadi, Andrew Birrell, Tim Harris, and Michael Isard. Semantics of transactional memory and automatic mutual exclusion.Proc. 35th. ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages(eds. George C. Necula and Philip Wadler), 63-74, ACM Press, 2008.","DOI":"10.1145\/1328438.1328449"},{"key":"10.2168\/LMCS-6(4:2)2010_TCS::AbadiP1993","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90151-I"},{"key":"10.2168\/LMCS-6(4:2)2010_AP09","doi-asserted-by":"crossref","unstructured":"Mart\u00edn Abadi and Gordon D. Plotkin. A model of cooperative threads.Proc. 36th. ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages(eds. Zhong Shao and Benjamin C. Pierce), 29-40, ACM Press, 2009.","DOI":"10.1145\/1480881.1480887"},{"key":"10.2168\/LMCS-6(4:2)2010_abrahamson:modal","first-page":"21","volume":"70","author":"Karl Abrahamson","year":"1979","journal-title":"Proc. Int. Symp. on Semantics of Concurrent Computation (ed. Gilles Kahn), Lect. Notes Comput. Sci.,"},{"key":"10.2168\/LMCS-6(4:2)2010_adya","unstructured":"Atul Adya, Jon Howell, Marvin Theimer, William J. Bolosky, and John R. Douceur. Cooperative task management without manual stack management.USENIXAnnual Technical Conf., General Track (ed. Carla Schlatter Ellis), 289-302, 2002."},{"key":"10.2168\/LMCS-6(4:2)2010_amadio:resource","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.01.017"},{"key":"10.2168\/LMCS-6(4:2)2010_BHM","first-page":"42","volume":"2395","author":"Nick Benton, John Hughes, and Eugenio Mo","year":"2002","journal-title":"{\\em Advanced Lectures from Int. Summer School on Applied Semantics} (eds. Gilles Barthe, Peter Dybjer, Lu\u00eds Pinto, and Jo\u00e3o Saraiva), Lect. Notes Comput. Sci., 2395:42-122, Springer, 2002"},{"key":"10.2168\/LMCS-6(4:2)2010_Boudol","first-page":"272","volume":"4703","author":"G\u00e9rard Boudol","year":"2007","journal-title":"Proc. 18th. Int. Conf. on Concurrency Theory} (eds. Lu{\u00ed Lect. Notes Comput. Sci., 4703:272-286, Springer, 2007"},{"key":"10.2168\/LMCS-6(4:2)2010_Boussinot06","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.919"},{"key":"10.2168\/LMCS-6(4:2)2010_IC::Brookes1996","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0056"},{"key":"10.2168\/LMCS-6(4:2)2010_charles:x10","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094852"},{"key":"10.2168\/LMCS-6(4:2)2010_CM","doi-asserted-by":"crossref","unstructured":"Pietro Cenciarelli and Eugenio Moggi. A syntactic approach to modularity in denotational semantics.Proc. 5th. Biennial Meeting on Category Theory and Computer Science, 1993. Kurusch Ebrahimi-Fard and Li Guo. Rota-Baxter Algebras and Dendriform Algebras.J. Pure Appl. Algebra, 212(2), 320-339, 2008.","DOI":"10.1016\/j.jpaa.2007.05.025"},{"key":"10.2168\/LMCS-6(4:2)2010_DBLP:journals\/tcs\/FerreiraH99","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00049-8"},{"key":"10.2168\/LMCS-6(4:2)2010_Foi07","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpaa.2006.06.005"},{"key":"10.2168\/LMCS-6(4:2)2010_majumdar09","doi-asserted-by":"crossref","unstructured":"Pierre Ganty, Rupak Majumdar, and Andrey Rybalchenko. Verifying liveness for asynchronous programs.Proc. 36th. ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages(eds. Zhong Shao and Benjamin C. Pierce), 102-113, ACM Press, 2009.","DOI":"10.1145\/1480881.1480895"},{"key":"10.2168\/LMCS-6(4:2)2010_harris:composable","doi-asserted-by":"crossref","unstructured":"Tim Harris, Simon Marlow, Simon Peyton-Jones, and Maurice Herlihy. Composable memory transactions.Proc. 10th. ACM SIGPLAN Symp. on Principles and Practice of Parallel Programming(eds. Keshav Pingali, Katherine A. Yelick and Andrew S. Grimshaw), 48-60, ACM Press, 2005.","DOI":"10.1145\/1065944.1065952"},{"key":"10.2168\/LMCS-6(4:2)2010_HennessyM:fulaspl","first-page":"108","volume":"74","author":"Matthew Hennessy and Gordon D. Plotkin","year":"1979","journal-title":"{\\em Proc. 8th. Symp. on Mathematical Foundations of Computer Science} (ed. J. Be\\v cv\u00e1\\v r), { Lect.\\ Notes Comput. Sci.}, 74:108-120, Springer, 1979"},{"key":"10.2168\/LMCS-6(4:2)2010_horita","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1095"},{"key":"10.2168\/LMCS-6(4:2)2010_HPP","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.03.013"},{"key":"10.2168\/LMCS-6(4:2)2010_isard:automatic","unstructured":"Michael Isard and Andrew Birrell. Automatic mutual exclusion.Proc. 11th. USENIX Workshop on Hot Topics in Operating Systems, 1-6, 2007."},{"key":"10.2168\/LMCS-6(4:2)2010_LICS::Jeffrey1995","doi-asserted-by":"crossref","unstructured":"Alan Jeffrey. A fully abstract semantics for a concurrent functional language with monadic types.Proc. 10th. Symp. on Logic in Computer Science, 255-264, IEEE Press, 1995.","DOI":"10.1109\/LICS.1995.523261"},{"key":"10.2168\/LMCS-6(4:2)2010_jeffreycore","unstructured":"Alan Jeffrey. Semantics for core Concurrent ML using computation types.Higher Order Operational Techniques in Semantics(eds. Andrew D. Gordon and Andrew M. Pitts), 55-90, Cambridge University Press, 1997."},{"key":"10.2168\/LMCS-6(4:2)2010_Jeffrey:FAM","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.10.012"},{"key":"10.2168\/LMCS-6(4:2)2010_majumdar07","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190266"},{"key":"10.2168\/LMCS-6(4:2)2010_Lod01","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45328-8_2"},{"key":"10.2168\/LMCS-6(4:2)2010_SQL","unstructured":"Microsoft. SQL Server 2005 books online. CLR Hosted Environment, at \\urlhttp:\/\/msdn.microsoft.com\/en-us\/library\/ms131047.aspx, 2007."},{"key":"10.2168\/LMCS-6(4:2)2010_essenceofcml","doi-asserted-by":"crossref","unstructured":"Prakash Panangaden and John H. Reppy. The essence of Concurrent ML.ML with Concurrency(ed. Flemming Nielson), 5-29, Springer, 1997.","DOI":"10.1007\/978-1-4612-2274-3_2"},{"key":"10.2168\/LMCS-6(4:2)2010_Plo06","doi-asserted-by":"crossref","unstructured":"Gordon D. Plotkin. Hennessy-Plotkin-Brookes Revisited.Proc. 26th. Foundations of Software Technology and Theoretical Computer Science(eds. S. Arun-Kumar & Naveen Garg), Lect. Notes Comput. Sci., 4337:4, Springer, 2006","DOI":"10.1007\/11944836_2"},{"key":"10.2168\/LMCS-6(4:2)2010_PP1","first-page":"373","volume":"2303","author":"Gordon Plotkin and John Power","year":"2002","journal-title":"Proc. 5th. Int. Conf. on Foundations of Software Science and Computation Structures} (eds. Mogens Nielsen and Uffe Engberg), {Lect. Notes Comput. Sci."},{"key":"10.2168\/LMCS-6(4:2)2010_PP2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"10.2168\/LMCS-6(4:2)2010_DBLP:conf\/lics\/PlotkinP08","first-page":"80","volume":"5502","author":"Gordon D. Plotkin and Matija Pretnar","year":"2009","journal-title":"Proc. 23rd. Symp. on Logic in Computer Science,"},{"key":"10.2168\/LMCS-6(4:2)2010_saraswat:x10","first-page":"353","volume":"3653","author":"Vijay A. Saraswat and Radha Jagadeesan","year":"2005","journal-title":"Proc. 16th. Int. Conf. on Concurrency Theory (eds. Mart\u00edn Abadi and Luca de Alfaro), { Lect. Notes Comput. Sci.}, 3653:353-367, Springer, 2005"},{"key":"10.2168\/LMCS-6(4:2)2010_shavit:software","doi-asserted-by":"crossref","unstructured":"Nir Shavit and Dan Touitou. Software transactional memory.Proc. 14th. Annual ACMSymp. on Principles of Distributed Computing, 204-213, ACM Press, 1995.","DOI":"10.1145\/224964.224987"},{"key":"10.2168\/LMCS-6(4:2)2010_smaragdakis:transactions","doi-asserted-by":"crossref","unstructured":"Yannis Smaragdakis, Anthony Kay, Reimer Behrends, and Michal Young. Transactions with isolation and cooperation.Proc. 22nd. Annual ACM SIGPLAN Conf. on Object-Oriented Programming, Systems, Languages, and Applications(eds. Richard P. Gabriel, David F. Bacon, Cristina Videira Lopes and Guy L. Steele Jr.), 191-210, ACM Press, 2007.","DOI":"10.1145\/1297027.1297042"},{"key":"10.2168\/LMCS-6(4:2)2010_capriccio","doi-asserted-by":"crossref","unstructured":"J. Robert von Behren, Jeremy Condit, Feng Zhou, George C. Necula, and Eric A. Brewer. Capriccio: scalable threads for Internet services.Proc. 19th. ACMSymp. on Operating Systems Principles (eds. Michael L. Scott and Larry L. Peterson), 268-281, ACM Press, 2003.","DOI":"10.1145\/1165389.945471"},{"key":"10.2168\/LMCS-6(4:2)2010_Winskel93","doi-asserted-by":"publisher","DOI":"10.1007\/11944836_2"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/700\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/700\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,28]],"date-time":"2025-02-28T07:00:59Z","timestamp":1740726059000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/700"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,10,20]]},"references-count":36,"URL":"https:\/\/doi.org\/10.2168\/lmcs-6(4:2)2010","relation":{"is-same-as":[{"id-type":"arxiv","id":"1009.2405","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1009.2405","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"doi","id":"10.1007\/978-3-319-71237-6_17","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,10,20]]},"article-number":"700"}}