Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Static Trace-Based Deadlock Analysis for Synchronous Mini-Go

  • Conference paper
  • First Online:
Programming Languages and Systems (APLAS 2016)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10017))

Included in the following conference series:

Abstract

We consider the problem of static deadlock detection for programs in the Go programming language which make use of synchronous channel communications. In our analysis, regular expressions extended with a fork operator capture the communication behavior of a program. Starting from a simple criterion that characterizes traces of deadlock-free programs, we develop automata-based methods to check for deadlock-freedom. The approach is implemented and evaluated with a series of examples.

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.

    http://arxiv.org/abs/1608.08330.

  2. 2.

    Recall that primitive send/receive communications are expressed in terms of select.

References

  1. Boyapati, C., Lee, R., Rinard, M.C.: Ownership types for safe programming: preventing data races and deadlocks. In: Proceedings of OOPSLA 2002, pp. 211–230. ACM (2002)

    Google Scholar 

  2. Brzozowski, J.A.: Derivatives of regular expressions. J. ACM 11(4), 481–494 (1964)

    Article  MathSciNet  MATH  Google Scholar 

  3. Christakis, M., Sagonas, K.: Detection of asynchronous message passing errors using static analysis. In: Rocha, R., Launchbury, J. (eds.) PADL 2011. LNCS, vol. 6539, pp. 5–18. Springer, Heidelberg (2011). doi:10.1007/978-3-642-18378-2_3

    Chapter  Google Scholar 

  4. Colby, C.: Analyzing the communication topology of concurrent programs. In: Proceedings of PEPM 1995, pp. 202–213. ACM (1995)

    Google Scholar 

  5. Engler, D.R., Ashcraft, K.: RacerX: effective, static detection of race conditions and deadlocks. In: Proceeding of SOSP 2003, pp. 237–252. ACM (2003)

    Google Scholar 

  6. The Go programming language. https://golang.org/

  7. Oracle: a tool for answering questions about go source code. https://godoc.org/golang.org/x/tools/cmd/oracle

  8. Gopherlyzer: Trace-based deadlock detection for mini-go. https://github.com/KaiSta/gopherlyzer

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

    Article  MathSciNet  MATH  Google Scholar 

  10. Huang, S.T.: A distributed deadlock detection algorithm for CSP-like communication. ACM Trans. Program. Lang. Syst. 12(1), 102–122 (1990)

    Article  Google Scholar 

  11. Kobayashi, N.: TyPiCal: type-based static analyzer for the Pi-Calculus. http://www-kb.is.s.u-tokyo.ac.jp/~koba/typical/

  12. Kobayashi, N.: Type-based information flow analysis for the pi-calculus. Acta Inf. 42(4–5), 291–347 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  13. Kobayashi, N.: A new type system for deadlock-free processes. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 233–247. Springer, Heidelberg (2006). doi:10.1007/11817949_16

    Chapter  Google Scholar 

  14. Ladkin, P.B., Simons, B.B.: Static deadlock analysis for CSP-type communications. In: Fussell, D.S., Malek, M. (eds.) Responsive Computer Systems: Steps Toward Fault-Tolerant Real-Time Systems, pp. 89–102. Springer, Boston (1995)

    Chapter  Google Scholar 

  15. Martel, M., Gengler, M.: Communication topology analysis for concurrent programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 265–286. Springer, Heidelberg (2000). doi:10.1007/10722468_16

    Chapter  Google Scholar 

  16. Mercouroff, N.: An algorithm for analyzing communicating processes. In: Brookes, S., Main, M., Melton, A., Mislove, M., Schmidt, D. (eds.) MFPS 1991. LNCS, vol. 598, pp. 312–325. Springer, Heidelberg (1992). doi:10.1007/3-540-55511-0_16

    Chapter  Google Scholar 

  17. Milner, R.: Communicating and Mobile Systems: The \(\pi \)-Calculus. Cambridge University Press, New York (1999)

    MATH  Google Scholar 

  18. Ng, N., Yoshida, N.: Static deadlock detection for concurrent go by global session graph synthesis. In: Proceedings of CC 2016, pp. 174–184. ACM (2016)

    Google Scholar 

  19. Nielson, H.R., Nielson, F.: Higher-order concurrent programs with finite communication topology. In: Proceedings of POPL 1994, pp. 84–97. ACM Press, January 1994

    Google Scholar 

  20. Reppy, J.H.: Concurrent Programming in ML. Cambridge University Press, New York (1999)

    Book  MATH  Google Scholar 

  21. Sulzmann, M., Thiemann, P.: Forkable regular expressions. In: Dediu, A.-H., Janoušek, J., Martín-Vide, C., Truthe, B. (eds.) LATA 2016. LNCS, vol. 9618, pp. 194–206. Springer, Heidelberg (2016). doi:10.1007/978-3-319-30000-9_15

    Chapter  Google Scholar 

  22. Williams, A., Thies, W., Ernst, M.D.: Static deadlock detection for Java libraries. In: Black, A.P. (ed.) ECOOP 2005. LNCS, vol. 3586, pp. 602–629. Springer, Heidelberg (2005). doi:10.1007/11531142_26

    Chapter  Google Scholar 

Download references

Acknowledgments

We thank the APLAS’16 reviewers for their constructive feedback.

Author information

Authors and Affiliations

  1. Faculty of Computer Science and Business Information Systems, Karlsruhe University of Applied Sciences, Moltkestrasse 30, 76133, Karlsruhe, Germany

    Kai Stadtmüller & Martin Sulzmann

  2. Faculty of Engineering, University of Freiburg, Georges-Köhler-Allee 079, 79110, Freiburg, Germany

    Peter Thiemann

Authors
  1. Kai Stadtmüller
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Martin Sulzmann
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Peter Thiemann
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Martin Sulzmann .

Editor information

Editors and Affiliations

  1. Kyoto University , Kyoto, Japan

    Atsushi Igarashi

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Stadtmüller, K., Sulzmann, M., Thiemann, P. (2016). Static Trace-Based Deadlock Analysis for Synchronous Mini-Go. In: Igarashi, A. (eds) Programming Languages and Systems. APLAS 2016. Lecture Notes in Computer Science(), vol 10017. Springer, Cham. https://doi.org/10.1007/978-3-319-47958-3_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-47958-3_7

  • Published:

  • Publisher Name: Springer, Cham

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation