Static Deadlock Detection for Go

Nicholas Ng / nicholascwng

Imperial College London

Go Programming Language

2

Concurrency in Go

CSP example ("Communicating Sequential Processes", Hoare 2004)
3

Concurrency in Go: Goroutines and Channels

// +build OMIT

package main

import (
	"fmt"
	"time"
)

func deepThought(replyCh chan int) {
    time.Sleep(75 * time.Millisecond)
    replyCh <- 42
}

func main() {
    ch := make(chan int)
    go deepThought(ch)  
    answer := <-ch
    fmt.Printf("The answer is %d\n", answer)
}
4

Deadlocks in Go

fatal error: all goroutines are asleep - deadlock!
// +build OMIT

package main

import (
	"fmt"
	"time"
)

func deepThought(replyCh chan int) {
    time.Sleep(75 * time.Millisecond)
    replyCh <- 42
}

func main() {
    ch := make(chan int)
    go deepThought(ch)
    answer := <-ch      
    fmt.Printf("The answer is %d\n", answer)
}
5

Go language runtime and tools

// From Go source code - https://github.com/golang/go
// File runtime/proc.go


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

Yes, but...

// +build OMIT

package main

import (
	"fmt"
	"time"
)

var (
	result int
)

func Send(ch chan<- int)                     { ch <- 42 }             // Send
func RecvAck(ch <-chan int, done chan<- int) { v := <-ch; done <- v } // Recv then Send

func main() {
    ch, done := make(chan int), make(chan int)
    go Send(ch)
    go RecvAck(ch, done)
    go RecvAck(ch, done) // OOPS

    // Anonymous goroutine: Some long running work (e.g. http service)
    go func() {
        for i := 0; i < 3; i++ {
            fmt.Println("Working #", i)
            time.Sleep(1 * time.Second)
        }
	}()
	result = <-done
	result = <-done // OOPS // HLoops
	fmt.Println("Result is ", result)
}
7

Static analysis of Go source code

1. Convert to SSA Intermediate Representation (golang.org/x/tools/go/ssa)
2. Extract communication (send/recv/select/close) as local types, ignore computation
3. Model as Communicating FSM (state machine)

8

SSA IR

SSA = Single Static Assignment
In short: variables are assigned once (updates = new version of variable)

func main():
0:                                                                entry P:0 S:0
    t0 = make chan int 0:int                                       chan int
    t1 = make chan int 0:int                                       chan int
    t2 = changetype chan<- int <- chan int (t0)                  chan<- int
    go Send(t2)
    t3 = changetype <-chan int <- chan int (t0)                  <-chan int
    t4 = changetype chan<- int <- chan int (t1)                  chan<- int
    go Recv(t3, t4)
    t5 = changetype <-chan int <- chan int (t0)                  <-chan int
    t6 = changetype chan<- int <- chan int (t1)                  chan<- int
    go Recv(t5, t6)
    go Work()
    t7 = <-t1                                                           int
    t8 = <-t1                                                           int
    return
9

Static Analysis

10

Communicating Finite State Machine

Aim: Global (Session) Graph Synthesis

Left: Communicating Finite State Machines; Right: Global graph - deadlocked vs. fixed (consistent)
11

// TODOs

Tons of stuff missing but works on most simple programs

12

Thank you

Nicholas Ng / nicholascwng

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.)