Static Deadlock Detection for Go

Nicholas Ng

Imperial College London

Go and concurrency

Don't communicate by sharing memory, share memory by communicating.

Avoid locks for high-level concurrency

Inspired by Hoare's Communicating Sequential Processes (CSP)

Expressive message-passing concurrency model

1

Concurrency

Concurrency is complicated

Concurrency bugs are hard to find and fix (write perfect code if you can!)

Our research aims to help avoid concurrency bugs as much as possible

2

Concurrency problems: deadlocks

fatal error: all goroutines are asleep - deadlock!

// +build OMIT

package main

import (
	"fmt"
	"time"
)

// Anonymous goroutine: Some long running work (e.g. http service)
func Work() {
	for i := 0; ; i++ {
		fmt.Println("Working #", i)
		time.Sleep(1 * time.Second)
	}
}

func Sender(ch chan<- int) {
    ch <- 42
}
func Receiver(ch <-chan int, done chan<- int) {
    done <- <-ch
}

func main() {
    ch := make(chan int)
    done := make(chan int)
    go Sender(ch)
    go Receiver(ch, done)
    go Receiver(ch, done) // Who is ch receiving from?

    fmt.Println("Done 1:", <-done)
    fmt.Println("Done 2:", <-done)
}
3

What causes a deadlock in Go?

Deadlock

A classic deadlock
4

Avoiding deadlocks

Rule of thumb: Make sure sender/receiver are matching and compatible

Sounds simple, so why is it difficult in practice?

5

Go runtime deadlock detector

func checkdead() {
...
    // -1 for sysmon
    run := sched.mcount - sched.nmidle - sched.nmidlelocked - 1
    if run > 0 {
        return
    }
...
    getg().m.throwing = -1 // do not dump full stacks
    throw("all goroutines are asleep - deadlock!")
}
6

Go runtime deadlock detector

If we add a benign, long-running goroutine to the mix..

// +build OMIT

package main

import (
	"fmt"
	"time"
)

func Sender(ch chan<- int) {
	ch <- 42
}

func Receiver(ch <-chan int, done chan<- int) {
	done <- <-ch
}

func main() {
    ch := make(chan int)
    done := make(chan int)
    go Sender(ch)
    go Receiver(ch, done)
    go Receiver(ch, done) // Who is ch receiving from?
    // Unreleated worker goroutine, keeps deadlock 'alive'
    go func() {
        for i := 0; i < 2; i++ {
            fmt.Println("Working #", i)
            time.Sleep(500 * time.Millisecond)
        }
        fmt.Println("-------- Worker finished --------")
    }()

    fmt.Println("Done 1:", <-done)
    fmt.Println("Done 2:", <-done)
}

local deadlock: some (but not all) goroutines are stuck

7

Building a better deadlock detector

What if we can...

8

Static deadlock detector

Tool developed based on our research

Analysed common concurrency patterns & open source projects

9

Static deadlock detector

Under the hood: Workflow of our static deadlock detector
10

Modelling concurrency

To find deadlocks in communication

Who better to ask than pioneers of concurrency?

11

Models of concurrency: Process calculi

Process calculi: canonical models for communication


Tony Hoare
  • Quicksort, Hoare Logic, etc.
  • CSP - Communicating Sequential Processes (1978)
  • Turing Award (1980)



Robin Milner
  • ML programming language, LCF, etc.
  • CCS - Calculus of Communicating Systems (1980)
  • π-calculus (1992)
  • Turing Award (1991)
12

Models of concurrency: Process calculi

Process calculi: canonical models for communication

Essence of communication: asynchronous π-calculus and Go
13

Models of concurrency: Process calculi

Process calculi: canonical models for communication

14

Types

// +build OMIT

package main

import (
	"fmt"
)

func main() {
    x := 42
    fmt.Printf("Type of x is %T", x)
    x = "hello" // incompatible!
}
Type checking: are the types compatible?
15

Types for communication (1/2)

Compatibility of communication
16

Types for communication (2/2)

Compatibility of communication
17

How to Go from code to model?

18

Extracting session types from code (1/2)

Static analysis: Look for make(chan T), ch <- x, <-ch, select, close

main

func main() {
    ch := make(chan int)
    done := make(chan int)

    go Sender(ch)
    go Receiver(ch, done)
    go Receiver(ch, done) // Who is ch receiving from?
    go Work() // Just an infinite loop

    fmt.Println("Done 1:", <-done)
    fmt.Println("Done 2:", <-done)
}
Session types for main()
19

Extracting session types from code (2/2)

Sender

func Sender(ch chan<- int) {
    ch <- 42
}

Receiver x 2

func Receiver(ch <-chan int, done chan<- int) {
    done <- <-ch
}

Worker (Non-communicating)

func() {          
    for i := 0; i < 4; i++ {
        fmt.Println("Working #", i)       
        time.Sleep(250 * time.Millisecond)
    }
}
20

Compose the model

Session types obtained from all goroutines in program

Next: compose and check compatibility

21

Global graph

Incompatible: this is not a well formed global graph

Note: the actual analysis is much more involved

22

Conclusion

References

📄 From Communicating Machines to Graphical Choreographies
J. Lange, E. Tuosto, N. Yoshida, POPL 2015

📄 Static Deadlock Detection for Go by Global Session Graph Synthesis
N. Ng, N. Yoshida, CC 2016

Thanks to my colleagues behind this work - Nobuko, Julien, Bernardo
23

Conclusion

More to come soon: more comprehensive theory and updated tool

Demo

24

Thank you

Nicholas Ng

Imperial College London

Use the left and right arrow keys or click the left and right edges of the page to navigate between slides.
(Press 'H' or navigate to hide this message.)