Skip to main content
SpringerLink
Log in

Fair Cooperative Multithreading

  • Conference paper
CONCUR 2007 – Concurrency Theory (CONCUR 2007)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4703))

Included in the following conference series:

Abstract

We propose a new operational model for shared variable concurrency, in the context of a concurrent, higher-order imperative language à la ML. In our model the scheduling of threads is cooperative, and a non-terminating process suspends itself on each recursive call. A property to ensure in such a model is fairness, that is, any thread should yield the scheduler after some finite computation. To this end, we follow and adapt the classical method for proving termination in typed formalisms, namely the realizability technique. There is a specific difficulty with higher-order state, which is that one cannot define a realizability interpretation simply by induction on types, because applying a function may have side-effects at types not smaller than the type of the function. Moreover, such higher-order side-effects may give rise to computations that diverge without resorting to explicit recursion. We overcome these difficulties by introducing a type and effect system for our language that enforces a stratification of the memory. The stratification prevents the circularities in the memory that may cause divergence, and allows us to define a realizability interpretation of the types and effects, which we then use to prove the intended termination property.

Work partially supported by the CRE FT-R&D no 46136511, and by the ANR-SETI-06-010 grant.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Adya, A., Howell, J., Theimer, M., Bolosky, W.J., Douceur, H.R.: Cooperative task management without manual stack management or, Event-driven programming is not the opposite of threaded programming, Usenix ATC (2002)

    Google Scholar 

  2. Anderson, T.E., Bershad, B.N., Lazowska, E.D., Levy, H.M.: Scheduler activations: effective kernel support for the user-level management of parallelism. ACM Trans. on Computer Systems 10(1), 53–79 (1992)

    Article  Google Scholar 

  3. Banga, G., Druschel, P., Mogul, J.C.: Better operating sytem features for faster network servers. ACM SIGMETRICS Performance Evaluation Review 26(3), 23–30 (1998)

    Article  Google Scholar 

  4. Barendregt, H.: Lambda Calculi with Types. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, pp. 117–309. Oxford University Press, Oxford (1992)

    Google Scholar 

  5. von Berhen, R., Condit, J., Brewer, E.: Why events are a bad idea (for highconcurrency servers). In: Proceedings of HotOS IX (2003)

    Google Scholar 

  6. von Berhen, R., Condit, J., Zhou, F., Necula, G.C., Brewer, E.: Capriccio: scalable threads for Internet services. In: SOSP 2003 (2003)

    Google Scholar 

  7. Benton, N., Leperchey, B.: Relational reasoning in a nominal semantics for storage. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 86–101. Springer, Heidelberg (2005)

    Google Scholar 

  8. Birkedal, L., Harper, R.: Relational interpretation of recursive types in an operational setting. Information and Computation 155(1-2), 3–63 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  9. Bohr, N., Birkedal, L.: Relational reasoning for recursive types and references. In: Kobayashi, N. (ed.) APLAS 2006. LNCS, vol. 4279, pp. 79–96. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  10. Boudol, G.: ULM, a core programming model for global computing. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 234–248. Springer, Heidelberg (2004)

    Google Scholar 

  11. Boudol, G.: On typing information flow. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, pp. 366–380. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  12. Boussinot, F.: FairThreads: mixing cooperative and preemptive threads in C. Concurrency and Computation: Practice and Experience 18, 445–469 (2006)

    Article  Google Scholar 

  13. Dabrowski, F., Boussinot, F.: Cooperative threads and preemptive computations. In: Proceeding of TV 2006, Workshop on Multithreading in Hardware and Software: Formal Approaches to Design and Verification, FLoC 2006 (2006)

    Google Scholar 

  14. Epardaud, S.: Mobile reactive programming in ULM. In: Proc. of the Fifth ACM SIGPLAN Workshop on Scheme and Functional Programming, pp. 87–98. ACM Press, New York (2004)

    Google Scholar 

  15. Filliâtre, J.-C.: Verification of non-functional programs using interpretations in type theory. J. Functional Programming 13(4), 709–745 (2003)

    Article  MATH  Google Scholar 

  16. Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science, vol. 7. Cambridge University Press, Cambridge (1989)

    MATH  Google Scholar 

  17. Kleene, S.C.: On the interpretation of intuitionistic number theory. J. of Symbolic Logic 10, 109–124 (1945)

    Article  MATH  MathSciNet  Google Scholar 

  18. Krivine, J.-L.: Lambda-Calcul: Types et Modèles, Masson, Paris (1990). English translation Lambda-Calculus, Types and Models, Ellis Horwood (1993)

    Google Scholar 

  19. Landin, P.J.: The mechanical evaluation of expressions. Computer Journal 6, 308–320 (1964)

    MATH  Google Scholar 

  20. Lucassen, J.M., Gifford, D.K.: Polymorphic effect systems. In: POPL 1988, pp. 47–57 (1988)

    Google Scholar 

  21. Mandel, L., Pouzet, M.: ReactiveML, a reactive extension to ML. In: PPDP 2005, pp. 82–93 (2005)

    Google Scholar 

  22. Mitchell, J.C.: Foundations for Programming Languages. MIT Press, Cambridge (1996)

    Google Scholar 

  23. Ousterhout, J.: Why threads are a bad idea (for most purposes), presentation given at the 1996 Usenix ATC (1996)

    Google Scholar 

  24. Pitts, A., Stark, I.: Operational reasoning for functions with local state. In: Gordon, A., Pitts, A. (eds.) Higher-Order Operational Techniques in Semantics, pp. 227–273. Publication of the Newton Institute, Cambridge Univ. Press (1998)

    Google Scholar 

  25. Plotkin, G.: Lambda-definability and logical relations. Memo SAI-RM-4, University of Edinburgh (1973)

    Google Scholar 

  26. Pucella, R.: Reactive programming in Standard ML. In: IEEE Intern. Conf. on Computer Languages, pp. 48–57. IEEE Computer Society Press, Los Alamitos (1998)

    Google Scholar 

  27. Sangiorgi, D.: Termination of processes. Math. Struct. in Comp. Science 16, 1–39 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  28. Serrano, M., Boussinot, F., Serpette, B.: Scheme fair threads. In: PPDP 2004, pp. 203–214 (2004)

    Google Scholar 

  29. Talpin, J.-P., Jouvelot, P.: The type and effect discipline. Information and Computation 111, 245–296 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  30. Tait, W.: Intensional interpretations of functionals of finite type I. J. of Symbolic Logic 32, 198–212 (1967)

    Article  MATH  MathSciNet  Google Scholar 

  31. Tait, W.: A realizability interpretation of the theory of species, Logic Colloquium. Lecture Notes in Mathematics, vol. 453, pp. 240–251 (1975)

    Google Scholar 

  32. Tofte, M., Talpin, J.-P.: Region-based memory management. Information and Computation 132(2), 109–176 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  33. Welsh, M., Culler, D., Brewer, E.: SEDA: an architecture for well-conditioned, scalable internet services. In: SOSP 2001, pp. 230–243 (2001)

    Google Scholar 

  34. Wright, A., Felleisen, M.: A syntactic approach to type soundness. Information and Computation 115(1), 38–94 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  35. Yoshida, N., Berger, M., Honda, K.: Strong normalisation in the π-calculus. Information and Computation 191(2), 145–202 (2004)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA, 06902 Sophia Antipolis, France

    Gérard Boudol

Authors
  1. Gérard Boudol
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Luís Caires Vasco T. Vasconcelos

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Boudol, G. (2007). Fair Cooperative Multithreading. In: Caires, L., Vasconcelos, V.T. (eds) CONCUR 2007 – Concurrency Theory. CONCUR 2007. Lecture Notes in Computer Science, vol 4703. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74407-8_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-74407-8_19

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-74406-1

  • Online ISBN: 978-3-540-74407-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation