Document Open Access Logo

Static Race Detection and Mutex Safety and Liveness for Go Programs

Authors Julia Gabet , Nobuko Yoshida

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2020.4.pdf
  • Filesize: 0.83 MB
  • 30 pages

Document Identifiers

Author Details

Julia Gabet
  • Imperial College London, United Kingdom
Nobuko Yoshida
  • Imperial College London, United Kingdom

Funding

The work is partially supported by VeTSS, EPSRC EP/K011715/1, EP/K034413/1, EP/L00058X/1, EP/N027833/1, EP/N028201/1, EP/T006544/1 and EP/T014709/1.

Acknowledgements

The authors want to thank Nicholas Ng for his initial collaboration on the project.

Cite AsGet BibTex

Julia Gabet and Nobuko Yoshida. Static Race Detection and Mutex Safety and Liveness for Go Programs. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 4:1-4:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.ECOOP.2020.4

Abstract

Go is a popular concurrent programming language thanks to its ability to efficiently combine concurrency and systems programming. In Go programs, a number of concurrency bugs can be caused by a mixture of data races and communication problems. In this paper, we develop a theory based on behavioural types to statically detect data races and deadlocks in Go programs. We first specify lock safety/liveness and data race properties over a Go program model, using the happens-before relation defined in the Go memory model. We represent these properties of programs in a μ-calculus model of types, and validate them using type-level model-checking. We then extend the framework to account for Go’s channels, and implement a static verification tool which can detect concurrency errors. This is, to the best of our knowledge, the first static verification framework of this kind for the Go language, uniformly analysing concurrency errors caused by a mix of shared memory accesses and asynchronous message-passing communications.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Concurrent programming languages
  • Software and its engineering → Model checking
  • Theory of computation → Process calculi
Keywords
  • Go language
  • behavioural types
  • race detection
  • happens-before relation
  • safety
  • liveness

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Godel 2 Benchmarks. URL: https://github.com/JujuYuki/godel2-benchmark.
  2. Godel 2. URL: https://github.com/JujuYuki/godel2.
  3. migoinfer+. URL: https://github.com/JujuYuki/gospal.
  4. Martin Abadi, Cormac Flanagan, and Stephen N. Freund. Types for safe locking: Static race detection for java. ACM Trans. Program. Lang. Syst., 28(2):207–255, March 2006. URL: https://doi.org/10.1145/1119479.1119480.
  5. Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre-Malo Deniélou, Simon J. Gay, Nils Gesbert, Elena Giachino, Raymond Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T. Vasconcelos, and Nobuko Yoshida. Behavioral Types in Programming Languages. Foundations and Trends in Programming Languages, 3(2-3), 2017. URL: https://doi.org/10.1561/2500000031.
  6. David Castro, Raymond Hu, Sung-Shik Jongmans, Nicholas Ng, and Nobuko Yoshida. Distributed Programming Using Role Parametric Session Types in Go. In 46th ACM SIGPLAN Symposium on Principles of Programming Languages, pages 1-30. ACM, 2019. URL: https://doi.org/10.1145/3290342.
  7. Sagar Chaki, Sriram K. Rajamani, and Jakob Rehof. Types as models: model checking message-passing programs. In POPL'02, pages 45-57, 2002. Google Scholar
  8. Sjoerd Cranen, Jan Friso Groote, Jeroen J. A. Keiren, Frank P. M. Stappers, Erik P. de Vink, Wieger Wesselink, and Tim A. C. Willemse. An Overview of the mCRL2 Toolset and Its Recent Advances, pages 199-213. Springer Berlin Heidelberg, Berlin, Heidelberg, 2013. URL: https://doi.org/10.1007/978-3-642-36742-7_15.
  9. Nicolas Dilley and Julien Lange. An empirical study of messaging passing concurrency in Go projects. In SANER. IEEE, 2019. Google Scholar
  10. Alan A.A. Donovan and Brian W. Kernighan. The Go Programming Language. Addison-Wesley Professional, 1st edition, 2015. Google Scholar
  11. Stephan Falke and Marc Brockschmidt. KITTeL/KoAT. https://github.com/s-falke/kittel-koat, 2018.
  12. Steve Francia. Nine years of Go. https://blog.golang.org/9years, 2018.
  13. Julia Gabet and Nobuko Yoshida. Static Race Detection and Mutex Safety and Liveness for Go Programs (extended version). CoRR, abs/2004.12859, 2020. URL: http://arxiv.org/abs/2004.12859.
  14. GitHub. The fastest growing languages, 2018. URL: http://octoverse.github.com/.
  15. Go. Data Race Detector. https://golang.org/doc/articles/race_detector.html, 2013.
  16. Go. The Go Memory Model. https://golang.org/ref/mem, 2014.
  17. Golang. mutex.go, 2019. URL: https://golang.org/src/sync/mutex.go.
  18. Golang. rwmutex.go, 2019. URL: https://golang.org/src/sync/rwmutex.go.
  19. Golang. The Go Programming Language, 2019. URL: https://golang.org.
  20. Jan Friso Groote and Mohammad Reza Mousavi. Modeling and Analysis of Communicating Systems. The MIT Press, 2014. Google Scholar
  21. Jonas Kastberg Hinrichsen, Jesper Bengtson, and Robbert Krebbers. Actris: Session-type based reasoning in separation logic. Proc. ACM Program. Lang., 4(POPL), December 2019. URL: https://doi.org/10.1145/3371074.
  22. C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985. Google Scholar
  23. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In POPL'08, pages 273-284. ACM, 2008. Google Scholar
  24. Atsushi Igarashi and Naoki Kobayashi. A generic type system for the pi-calculus. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '01, pages 128-141, New York, NY, USA, 2001. ACM. URL: https://doi.org/10.1145/360204.360215.
  25. Klaus v. Gleissenthall and Rami Gökhan Kıcı and Alexander Bakst and Deian Stefan and Ranjit Jhala. Pretend synchrony: Synchronous verification of asynchronous distributed programs. Proc. ACM Program. Lang., 3(POPL):59:1-59:30, January 2019. URL: https://doi.org/10.1145/3290372.
  26. Naoki Kobayashi and Davide Sangiorgi. A hybrid type system for lock-freedom of mobile processes. ACM Trans. Program. Lang. Syst., 32(5), May 2008. URL: https://doi.org/10.1145/1745312.1745313.
  27. Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. Fencing off Go: Liveness and safety for channel-based programming. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pages 748-761. ACM, 2017. URL: https://doi.org/10.1145/3009837.3009847.
  28. Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. A static verification framework for message passing in go using behavioural types. In Proceedings of the 40th International Conference on Software Engineering, ICSE '18, pages 1137-1148, New York, NY, USA, 2018. ACM. URL: https://doi.org/10.1145/3180155.3180157.
  29. Bozhen Liu and Jeff Huang. D4: Fast concurrency debugging with parallel differential analysis. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, pages 359-373, New York, NY, USA, 2018. ACM. URL: https://doi.org/10.1145/3192366.3192390.
  30. Jan Midtgaard, Flemming Nielson, and Hanne Riis Nielson. Process-local static analysis of synchronous processes. In Andreas Podelski, editor, Static Analysis, pages 284-305, Cham, 2018. Springer International Publishing. Google Scholar
  31. Robin Milner. A Calculus of Communicating Systems, volume 92. Springer-Verlag, 1980. Google Scholar
  32. Robin Milner and Davide Sangiorgi. Barbed bisimulation. In Proc. ICALP'92, volume 623 of LNCS, 1992. Google Scholar
  33. Nicholas Ng and Nobuko Yoshida. Static Deadlock Detection for Concurrent Go by Global Session Graph Synthesis. In CC 2016, pages 174-184. ACM, 2016. Google Scholar
  34. Hanne Riis Nielson and Flemming Nielson. Higher-order concurrent programs with finite communication topology (extended abstract). In POPL, 1994. URL: https://doi.org/10.1145/174675.174538.
  35. Rob Pike. Go at Google. In SPLASH, pages 5-6, New York, NY, USA, 2012. ACM. Google Scholar
  36. Davide Sangiorgi and David Walker. The π-Calculus: a Theory of Mobile Processes. Cambridge University Press, 2001. Google Scholar
  37. Alceste Scalas and Nobuko Yoshida. Less Is More: Multiparty Session Types Revisited. In 46th ACM SIGPLAN Symposium on Principles of Programming Languages, pages 1-29. ACM, 2019. Google Scholar
  38. Alceste Scalas, Nobuko Yoshida, and Elias Benussi. Verifying message-passing programs with dependent behavioural types. In Programming Language Design and Implementation, 2019. Google Scholar
  39. Scribble. Scribble Project, 2008. URL: https://www.scribble.org.
  40. Konstantin Serebryany and Timur Iskhodzhanov. ThreadSanitizer: Data race detection in practice. In Proceedings of the Workshop on Binary Instrumentation and Applications, WBIA '09, pages 62-71, New York, NY, USA, 2009. ACM. URL: https://doi.org/10.1145/1791194.1791203.
  41. Konstantin Serebryany, Alexander Potapenko, Timur Iskhodzhanov, and Dmitriy Vyukov. Dynamic race detection with LLVM compiler. In Proceedings of the Second International Conference on Runtime Verification, RV'11, pages 110-114, Berlin, Heidelberg, 2012. Springer-Verlag. URL: https://doi.org/10.1007/978-3-642-29860-8_9.
  42. Kai Stadmüller, Martin Sulzmann, and Peter Thiemann. Static Trace-Based Deadlock Analysis for Synchronous Mini-Go. In APLAS, volume 10017 of LNCS, 2016. Google Scholar
  43. Syzkaller. Randomized testing for Go. https://github.com/google/syzkaller, 2015.
  44. Technische Universiteit Eindhoven. mCRL2. https://www.mcrl2.org/web/user_manual/index.html, 2018.
  45. The Clang Team. ThreadSanitizer. http://clang.llvm.org/docs/ThreadSanitizer.html, 2015.
  46. Tengfei Tu, Xiaoyu Liu, Linhai Song, and Yiying Zhang. Understanding real-world concurrency bugs in Go. In Proceedings of the Twenty-Fourth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS '19, pages 865-878, New York, NY, USA, 2019. ACM. URL: https://doi.org/10.1145/3297858.3304069.
  47. Dmitry Vyukov. Randomized testing for Go. https://github.com/dvyukov/go-fuzz, 2015.
  48. Dmitry Vyukov and Andrew Gerrand. Introducing the Go Race Detector. https://blog.golang.org/race-detector, 2013.
  49. Sheng Zhan and Jeff Huang. Echo: Instantaneous in situ race detection in the IDE. In Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016, pages 775-786, New York, NY, USA, 2016. ACM. URL: https://doi.org/10.1145/2950290.2950332.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact