Skip to main content
SpringerLink
Log in

A Small-Step Semantics of a Concurrent Calculus with Goroutines and Deferred Functions

  • Chapter
  • First Online:
Theory and Practice of Formal Methods

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

Abstract

In this paper, we present a small-step operational semantics for a small concurrent language supporting deferred function calls and related constructs in the style of the Go programming language. For lexical scoping, the presence of higher-order functions, but also the presence of the \(\mathrel {\mathtt {defer}}\)-command, requires the notion of closures in the semantics.

The work was partially supported by the Norwegian-German bilateral PPP project GoRETech (“Go Runtime Enforcement Techniques”).

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 EPUB and 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

Notes

  1. 1.

    There’s an exception to this guarantee, though. Deferred code is executed independent from whether the goroutine panics or not, but it’s executed only if the enclosing stack frame returns. Divergence may prevent that, and another reason for failing to return is that the goroutine containing the deferred code may be terminated due to the fact that its parent goroutine terminates. See Sect. 2.2.2.

  2. 2.

    In other languages, an alternative semantics for closures exists as well, where, when building the closure, the non-local variables obtain their meaning passing them “by value” instead. Of course, a by-value treatment would make it impossible for deferred code to change the return value, after the main body has been exited, for instance due to a panic. Passing by value can be achieved here by handing over the value explicitly as an extra formal parameter, effectively using a “\(\lambda \)-lifted” version of the deferred code. Indeed, \(\lambda \)-lifting is a transformation used to give semantics to higher-order functions under lexical scoping [27] and an alternative to closures.

  3. 3.

    With the exception that deferred code can be used to change the value of return parameters declared in the function’s signature.

  4. 4.

    Running the example as is, where the main goroutine does not do much else than spawning two child goroutines, it is practically guaranteed that the parent (and with it the child goroutines) terminates before the children start affecting z.

References

  1. Ábrahám, E., de Boer, F.S., de Roever, W.-P., Steffen, M.: A deductive proof system for multithreaded Java with exceptions. Fundam. Informaticae 82(4), 391–463 (2008). (73 pages), An extended version of the 2005 conference contribution to FSEN 2005 and a reworked and shortened version of the University of Kiel, Department of Computer Science Technical report 0303

    MathSciNet  MATH  Google Scholar 

  2. America, P.: Issues in the design of a parallel object-oriented language. Formal Aspects Comput. 1(4), 366–411 (1989)

    Article  MATH  Google Scholar 

  3. Ancona, D., Lagorio, G., Zucca, E.: A core calculus for Java exceptions. SIGPLAN Not. 36, 16–30 (2001)

    Article  Google Scholar 

  4. Anton, K., Thiemann, P.: Typing coroutines. In: Page, R., Horváth, Z., Zsók, V. (eds.) TFP 2010. LNCS, vol. 6546, pp. 16–30. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  5. Baker, H., Hewitt, C.: The incremental garbage collection of processes. ACM Sigplan Not. 12, 55–59 (1977)

    Article  Google Scholar 

  6. Belsnes, D., Østvold, B.M.: Mixing threads and coroutines, Unpublished manuscript (2005)

    Google Scholar 

  7. Berdine, J., O’Hearn, P., Reddy, U., Thielecke, H.: Linear continuation-passing. Higher-Order Symbolic Comput. 15(2–3), 181–208 (2002)

    Article  MATH  Google Scholar 

  8. Conway, E.M.: Design of a separable transition-diagram compiler. Commun. ACM 6(7), 396–408 (1963)

    Article  MATH  Google Scholar 

  9. Dahl, O.-J., Myhrhaug, B., Nygaard, K.: Simula 67, common base language. Technical report S-2, Norsk Regnesentral (Norwegian Computing Center), Oslo, Norway, May 1968

    Google Scholar 

  10. de Boer, F.S.: Reasoning about Dynamically Evolving Process Structures. A Proof Theory for the Parallel Object-Oriented Language POOL. Ph.D. thesis, Free University of Amsterdam (1991)

    Google Scholar 

  11. de Boer, F.S., Clarke, D., Johnsen, E.B.: A complete guide to the future. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 316–330. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  12. de Moura, A.L., Rodriguez, N., Ierusalimschy, R.: Coroutines in Lua. J. Univ. Comput. Sci. 10, 910–925 (2004)

    Google Scholar 

  13. Donovan, A.A.A., Kernighan, B.W.: The Go Programming Language. Addison-Wesley (2015)

    Google Scholar 

  14. Evans Jr., A.: PAL – a language designed for teaching programming linguistics. In: Proceedings of the 1968 23rd ACM National Conference, pp. 395–403. ACM, New York (1968)

    Google Scholar 

  15. Evans Jr., A.: PAL: pedagogic algorithmic language: a reference manual and primer. Unpublished report, Department of Electrical Engineering, MIT (1968)

    Google Scholar 

  16. Felleisen, M., Friedman, D.P.: Control operators, the SECD-machine, and the \(\lambda \)-calculus. In: Wirsing, M. (ed.) Formal Description of Programming Concepts III, pp. 193–217. North-Holland, Amsterdam (1986)

    Google Scholar 

  17. Flanagan, C., Sabry, A., Duba, B.F., Felleisen, M.: The essence of compiling with continuations. In: ACM Conference on Programming Language Design and Implementation (PLDI), pp. 237–247. ACM, June 1993. In SIGPLAN Notices 28(6)

    Google Scholar 

  18. The Go programming language specification, August 2015. https://golang.org/ref/spec

  19. Google. The Go programming language (2014). www.golang.org

  20. Gordon, A.D., Hankin, P.D., Lassen, S.B.: Compilation and equivalence of imperative objects. In: Ramesh, S., Sivakumar, G. (eds.) FST TCS 1997. LNCS, vol. 1346, pp. 74–87. Springer, Heidelberg (1997). Full version available as Technical report 429, University of Cambridge Computer Laboratory, June 1997

    Chapter  Google Scholar 

  21. Halstead Jr., R.H.: Multilisp: a language for concurrent symbolic computation. ACM Trans. Program. Lang. Syst. 7(4), 501–538 (1985)

    Article  MATH  Google Scholar 

  22. Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666–677 (1978)

    Article  MathSciNet  MATH  Google Scholar 

  23. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)

    MATH  Google Scholar 

  24. Apple Inc.: Swift. A modern programming language that is safe, fast, and interactive, October 2015. https://developer.apple.com/swift/

  25. Jeannin, J.B.: Capsules and closures: a small-step approach. Electron. Notes Theor. Comput. Sci. 276, 191–293 (2011). Proceedings of the Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVII)

    Article  MathSciNet  MATH  Google Scholar 

  26. Jeannin, J.B., Kozen, D.: Computing with capsules. Technical report, Computing and Information Science, Cornell University, January 2011

    Google Scholar 

  27. Johnsson, T.: Lambda lifting: transforming programs to recursive equations. In: Jouannaud, J.-P. (ed.) FPCA 1985. LNCS, vol. 201, pp. 190–203. Springer, Heidelberg (1985)

    Chapter  Google Scholar 

  28. Laird, J.: A calculus of coroutines. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 882–893. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  29. Landin, P.J.: The mechanical evaluation of expressions. Comput. J. 6(4), 308–320 (1964)

    Article  MATH  Google Scholar 

  30. Liu, H., Qiu, Z.: Go model and object oriented programming. In: Pardo, A., et al. (eds.) SBLP 2015. LNCS, vol. 9325, pp. 59–74. Springer, Heidelberg (2015). doi:10.1007/978-3-319-24012-1_5

    Chapter  Google Scholar 

  31. Malayeri, D., Aldrich, J.: Integrating nominal and structural subtyping. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol. 5142, pp. 260–285. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  32. Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, part I/II. Inf. Comput. 100, 1–77 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  33. Reus, B., Streicher, T.: About hoare logics for higher-order store. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1337–1348. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  34. Steele, G.L., Sussman, G.J., Scheme: an interpreter for the extended lambda calculus. AI Memo 349, MIT Artificial Intelligence Laboratory (1975)

    Google Scholar 

  35. Steele, G.L., Sussman, G.J.: Scheme: an interpreter for the extended lambda calculus. High.-Order Symbolic Computat. 11, 405–439 (1998)

    Article  MATH  Google Scholar 

  36. Summerfield, M.: Programming in Go. Addison-Wesley, Upper Saddle River (2012)

    Google Scholar 

  37. Wang, A., Dahl, O.-J.: Coroutine sequencing in a block structured environment. BIT Numer. Meth. 11(4), 425–449 (1971)

    Article  MATH  Google Scholar 

Download references

Acknowledgments

I am also grateful for the thorough, insightful, and detailed feedback from the anonymous reviewers which helped improving the paper.

Author information

Authors and Affiliations

  1. Department of Informatics, University of Oslo, Oslo, Norway

    Martin Steffen

Authors
  1. Martin Steffen
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Martin Steffen .

Editor information

Editors and Affiliations

  1. Informatik 2, RWTH Aachen University Informatik 2, Aachen, Germany

    Erika Ábrahám

  2. Leiden University , Leiden, The Netherlands

    Marcello Bonsangue

  3. University of Oslo , Oslo, Norway

    Einar Broch Johnsen

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Steffen, M. (2016). A Small-Step Semantics of a Concurrent Calculus with Goroutines and Deferred Functions. In: Ábrahám, E., Bonsangue, M., Johnsen, E. (eds) Theory and Practice of Formal Methods. Lecture Notes in Computer Science(), vol 9660. Springer, Cham. https://doi.org/10.1007/978-3-319-30734-3_26

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-30734-3_26

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-30733-6

  • Online ISBN: 978-3-319-30734-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation