Martin Abadi
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.
- Mart'ın Abadi, Andrew Birrell, Tim Harris, and Michael Isard. Semantics of transactional memory and automatic mutual exclusion. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 63--74, 2008. Google Scholar
Digital Library
- Mart'ın Abadi and Gordon D. Plotkin. A logical view of composition. Theoretical Computer Science, 114(1):3--30, June 1993. Google ScholarDigital Library
- Karl Abrahamson. Modal logic of concurrent nondeterministic programs. In Gilles Kahn, editor, International Symposium on Semantics of Concurrent Computation, volume 70 of Lecture Notes in Computer Science, pages 21-33. Springer, 1979. Google ScholarDigital Library
- Atul Adya, Jon Howell, Marvin Theimer, William J. Bolosky, and John R. Douceur. Cooperative task management without manual stack management. In Proceedings of the General Track: the 2002 USENIX Annual Technical Conference, pages 289-302, 2002. Google ScholarDigital Library
- Roberto Amadio and Silvano Dal Zilio. Resource control for synchronous cooperative threads. Theoretical Computer Science, 358:229--254, 2006. Google ScholarDigital Library
- Nick Benton, John Hughes, and Eugenio Moggi. Monads and effects. In Gilles Barthe, Peter Dybjer, Lu'ıs Pinto, and João Saraiva, editors, Advanced Lectures from International Summer School on Applied Semantics, volume 2395 of Lecture Notes in Computer Science, pages 42--122. Springer, 2002. Google ScholarDigital Library
- Dave Berry, Robin Milner, and David N. Turner. A semantics for ML concurrency primitives. In Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 119--129, 1992. Google ScholarDigital Library
- Gérard Boudol. Fair cooperative multithreading. In Luís Caires and Vasco Thudichum Vasconcelos, editors, Concurrency Theory, 18th International Conference, volume 4703 of Lecture Notes in Computer Science, pages 272--286. Springer, 2007. Google ScholarDigital Library
- Fréderic Boussinot. Fairthreads: mixing cooperative and preemptive threads in C. Concurrency and Computation: Practice and Experience, 18(5):445--469, April 2006. Google ScholarDigital Library
- Stephen Brookes. Full abstraction for a shared-variable parallel language. Information and Computation, 127(2):145--163, June 1996.Google ScholarCross Ref
- Stephen Brookes. The essence of parallel Algol. Information and Computation, 179(1):118--149, 2002. Google ScholarDigital Library
- Pietro Cenciarelli and Eugenio Moggi. A syntactic approach to modularity in denotational semantics. In Proceedings of the 5th Biennial Meeting on Category Theory and Computer Science, 1993.Google Scholar
- William Ferreira and Matthew Hennessy. A behavioural theory of first-order CML. Theoretical Computer Science, 216(1-2):55--107, 1999. Google ScholarDigital Library
- Tim Harris, Simon Marlow, Simon Peyton-Jones, and Maurice Herlihy. Composable memory transactions. In Proceedings of the 10th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pages 48--60, 2005. Google ScholarDigital Library
- Matthew Hennessy and Gordon D. Plotkin. Full abstraction for a simple programming language. In J. Bećvář, editor, 8th Symposium on Mathematical Foundations of Computer Science, volume 74 of Lecture Notes in Computer Science, pages 108--120. Springer, 1979.Google Scholar
- E. Horita, J. W. de Bakker, and J. J. M. M. Rutten. Fully abstract denotational models for nonuniform concurrent languages. Information and Computation, 115(1):125--178, 1994. Google ScholarDigital Library
- Martin Hyland, Gordon Plotkin, and John Power. Combining effects: Sum and tensor. Theoretical Computer Science, 357(1-3):70--99, 2006. Google ScholarDigital Library
- Michael Isard and Andrew Birrell. Automatic mutual exclusion. In Proceedings of the 11th USENIX workshop on Hot Topics in Operating Systems, pages 1--6, 2007. Google ScholarDigital Library
- Alan Jeffrey. A fully abstract semantics for a concurrent functional language with monadic types. In Proceedings, Tenth Annual IEEE Symposium on Logic in Computer Science, pages 255--264, 1995. Google ScholarDigital Library
- Alan Jeffrey. Semantics for core Concurrent ML using computation types. In Higher order operational techniques in semantics, pages 55--90. Cambridge University Press, 1997. Google ScholarDigital Library
- Alan Jeffrey and Julian Rathke. A fully abstract may testing semantics for concurrent objects. Theoretical Computer Science, 338(1-3):17--63, June 2005. Google ScholarDigital Library
- Microsoft. SQL Server 2005 books online. CLR Hosted Environment, at http://msdn.microsoft.com/en-us/library/ms131047.aspx, September 2007.Google Scholar
- Prakash Panangaden and John H. Reppy. The essence of Concurrent ML. In Flemming Nielson, editor, ML with Concurrency, chapter 1, pages 5--29. Springer, 1997.Google Scholar
- Gordon Plotkin and John Power. Notions of computation determine monads. Lecture Notes in Computer Science, 2303:373--393, 2002. Google ScholarDigital Library
- Gordon D. Plotkin and John Power. Algebraic operations and generic effects. Applied Categorical Structures, 11(1):69--94, 2003.Google ScholarCross Ref
- Gordon D. Plotkin and Matija Pretnar. A logic for algebraic effects. In Proceedings, Twenty-Third Annual IEEE Symposium on Logic in Computer Science, pages 118--129, 2008. Google ScholarDigital Library
- Nir Shavit and Dan Touitou. Software transactional memory. In Proceedings of the 14th Annual ACM Symposium on Principles of Distributed Computing, pages 204--213, 1995. Google ScholarDigital Library
- Yannis Smaragdakis, Anthony Kay, Reimer Behrends, and Michal Young. Transactions with isolation and cooperation. In Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 191--210, 2007. Google ScholarDigital Library
- J. Robert von Behren, Jeremy Condit, Feng Zhou, George C. Necula, and Eric A. Brewer. Capriccio: scalable threads for Internet services. In Proceedings of the 19th ACM Symposium on Operating Systems Principles, pages 268--281, 2003. Google ScholarDigital Library
- Glynn Winskel. The Formal Semantics of Programming Languages. The MIT Press, 1993. Google ScholarDigital Library
Index Terms
- A model of cooperative threads
Recommendations
A model of cooperative threads
POPL '09We 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 ...
Full Abstractness of a Metric Semantics for Action Refinement
For a process language with action refinement and synchronization both an operational and a denotational semantics are given. The operational semantics is based on an SOS-style transition system specification involving syntactical refinement sequences. ...
Algebraic approach to linking the semantics of web services
Web services have become more and more important in these years, and BPEL4WS (BPEL) is a de facto standard for the web service composition and orchestration. It contains several distinct features, including the scope-based compensation and fault ...
Comments