A model of cooperative threads

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.

REFERENCES

• 1: Martín Abadi , Andrew Birrell , Tim Harris , Michael Isard, Semantics of transactional memory and automatic mutual exclusion, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 2: Martín Abadi , Gordon D. Plotkin, A logical view of composition, Theoretical Computer Science, v.114 n.1, p.3-30, June 14 1993
• 3: Karl R. Abrahamson, Modal Logic of Concurrent Nondeterministic Programs, Proceedings of the International Sympoisum on Semantics of Concurrent Computation, p.21-33, July 02-04, 1979
• 4: Atul Adya , Jon Howell , Marvin Theimer , William J. Bolosky , John R. Douceur, Cooperative Task Management Without Manual Stack Management, Proceedings of the General Track of the annual conference on USENIX Annual Technical Conference, p.289-302, June 10-15, 2002
• 5: Roberto M. Amadio , Silvano Dal Zilio, Resource control for synchronous cooperative threads, Theoretical Computer Science, v.358 n.2, p.229-254, 7 August 2006 [doi>10.1016/j.tcs.2006.01.017]
• 6: Nick Benton , John Hughes , Eugenio Moggi, Monads and Effects, Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures, p.42-122, September 09-15, 2000
• 7: Dave Berry , Robin Milner , David N. Turner, A semantics for ML concurrency primitives, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.119-129, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143191]
• 8: 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.
• 9: Frédéric Boussinot, FairThreads: mixing cooperative and preemptive threads in C: Research Articles, Concurrency and Computation: Practice & Experience, v.18 n.5, p.445-469, April 2006 [doi>10.1002/cpe.v18:5]
• 10: Stephen Brookes. Full abstraction for a shared-variable parallel language. Information and Computation, 127(2):145--163, June 1996.
• 11: Stephen Brookes, The essence of parallel Algol, Information and Computation, v.179 n.1, p.118-149, November 25, 2002 [doi>10.1006/inco.2002.2995]
• 12: 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.
• 13: William Ferreira , Matthew Hennessy, A behavioural theory of first-order CML, Theoretical Computer Science, v.216 n.1-2, p.55-107, March 11, 1999 [doi>10.1016/S0304-3975(98)00049-8]
• 14: Tim Harris , Simon Marlow , Simon Peyton-Jones , Maurice Herlihy, Composable memory transactions, Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 15-17, 2005, Chicago, IL, USA [doi>10.1145/1065944.1065952]
• 15: 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.
• 16: E. Horita , J. W. de Bakker , J. J. M. M. Rutten, Fully abstract denotational models for nonuniform concurrent languages, Information and Computation, v.115 n.1, p.125-178, Nov. 15, 1994 [doi>10.1006/inco.1994.1095]
• 17: Martin Hyland , Gordon Plotkin , John Power, Combining effects: sum and tensor, Theoretical Computer Science, v.357 n.1, p.70-99, 25 July 2006 [doi>10.1016/j.tcs.2006.03.013]
• 18: Michael Isard , Andrew Birrell, Automatic mutual exclusion, Proceedings of the 11th USENIX workshop on Hot topics in operating systems, p.1-6, May 07-09, 2007, San Diego, CA
• 19: Alan Jeffrey, A Fully Abstract Semantics for a Concurrent Functional Language with Monadic Types, Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, p.255, June 26-29, 1995
• 20: A. Jeffrey, Semantics for core Concurrent ML using computation types, Higher order operational techniques in semantics, Cambridge University Press, New York, NY, 1999
• 21: Alan Jeffrey , Julian Rathke, A fully abstract may testing semantics for concurrent objects, Theoretical Computer Science, v.338 n.1-3, p.17-63, 10 June 2005 [doi>10.1016/j.tcs.2004.10.012]
• 22: Microsoft. SQL Server 2005 books online. CLR Hosted Environment, at http://msdn.microsoft.com/en-us/library/ms131047.aspx, September 2007.
• 23: 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.
• 24: Gordon D. Plotkin , John Power, Notions of Computation Determine Monads, Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures, p.342-356, April 08-12, 2002
• 25: Gordon D. Plotkin and John Power. Algebraic operations and generic effects. Applied Categorical Structures, 11(1):69--94, 2003.
• 26: Gordon Plotkin , Matija Pretnar, A Logic for Algebraic Effects, Proceedings of the 2008 23rd Annual IEEE Symposium on Logic in Computer Science, p.118-129, June 24-27, 2008 [doi>10.1109/LICS.2008.45]
• 27: Nir Shavit , Dan Touitou, Software transactional memory, Proceedings of the fourteenth annual ACM symposium on Principles of distributed computing, p.204-213, August 20-23, 1995, Ottowa, Ontario, Canada [doi>10.1145/224964.224987]
• 28: Yannis Smaragdakis , Anthony Kay , Reimer Behrends , Michal Young, Transactions with isolation and cooperation, Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems and applications, October 21-25, 2007, Montreal, Quebec, Canada
• 29: Rob von Behren , Jeremy Condit , Feng Zhou , George C. Necula , Eric Brewer, Capriccio: scalable threads for internet services, Proceedings of the nineteenth ACM symposium on Operating systems principles, October 19-22, 2003, Bolton Landing, NY, USA
• 30: Glynn Winskel, The formal semantics of programming languages: an introduction, MIT Press, Cambridge, MA, 1993

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.3 Concurrent Programming
          Subjects: Parallel programming

General Terms:
Languages, Theory

Keywords:
denotational semantics, monad, operational semantics, transaction