PI: Nobuko Yoshida, PhD Student: Julia Gabet, Imperial College London

  • Concurrent programs introduce a specific class of bugs relating to memory safety and deadlocks.
  • Detection of concurrency bugs in Go and other concurrent languages often relies on runtime analysing with fuzzing techniques, making it unreliable and allowing bugs to make it to the production software. 
  • Static detection frameworks allow to reduce the fraction of those bugs that make it to production stages, by consistently analysing a session types model of the source code against properties based on behavioural and memory models of the target language. 
  • Coupling both techniques allows for an increase in robustness for the development chain of trusted software, ensuring a lesser number of critical bugs end up in production.

Go is a concurrent programming language developed in recent years by Google. It is used by various projects, including cloud service providers like Twitter and Dropbox, open source projects including Docker, Kubernetes and CoreOS. This increasing popularity is reflected on Go’s position in several programming language’s rankings, including IEEE Spectrum Top Programming Languages (from place 20 in 2014 to 9 in 2017), StackOverflow’s most loved and most wanted languages (5th and 3rd place resp., in 2018), and Github’s top growing languages (where it ranked 7th in 2018). Go’s most appreciated features are notably its concurrency features, including channel-based message-passing and lightweight thread creation features. These features, however, make programmers struggle with bugs such as communication deadlocks, message mismatches or memory safety issues.

This project builds on the foundations laid by works on detection of channel-based concurrency issues, and brings them further by proving the theoretical base of these works and extending it greatly. Our recent work tackles both channel-based concurrency issues (including deadlocks and safe channel usage) and shared memory-based issued, especially revolving on the correct usage of mutual exclusion locks and data race detection. We use Go’s official memory model detailed in the documentation of the language, extracting from it a happens-before relation that is used to define how a data race can be statically detected.

We also formally prove the equivalence between properties of our abstracted types and properties of the source language, defining precisely what conditions programs need to meet so they can be correctly analysed by our framework. This framework is then implemented in a tool, Godel 2, the workflow of which is described in the figure on the right. It uses the mCRL2 model checker and the KiTTEL termination checker to verify the properties we extract from the code against the model behavioural-types we infer from program source code.

The approach used in this project can be extended to a toolchain, Scribble, a protocol description language based on Multiparty Session Types, that is used to design and verify protocols and their implementations. Scribble is used by teams and projects in companies such as Red Hat and Estafet to genenerate deadlock-free microservices in Go.

PUBLICATIONS. [1] J. Gabet and N. Yoshida,  “Static Race Detection and Mutex Safety and Liveness for Go Programs, ECOOP 2020.” [2] R. Griesemer, R. Hu, W. Kokke, J. Lange, I.L. Taylor, B. Toninho, P. Wadler and N. Yoshida, “Featherweight Go”, OOPSLA 2020. [3] D. Castro, R. Hu, S. Jongmans, N. Ng and N. Yoshida, “Distributed Programming Using Role Parametric Session Types in Go”, POPL 2019.

RELATED GRANTS. Nobuko Yoshida, PI, EPSRC Established Career Fellowship: “POST: Protocols, Observabilities and Session Types”, 04/2020-03/2025, £1.46M; JSPS Invitation Fellowship for Research in Japan, £7,000, 07-08/2019.

IMPACT. “I want to thank you and your team for all the type theory work on Go so far — it really helped clarify our understanding to a massive degree. So thanks!” – R. Griesemer, Google USA, to P. Wadler about the work on Featherweight Go.