Static Deadlock Detection for Go by Global Session Graph Synthesis

Nicholas Ng & Nobuko Yoshida

Department of Computing

Imperial College London

Contributions

1

Go and Concurrency

" Do not communicate by sharing memory; instead, share memory by communicating. "
-- Effective Go (developer guide)

2

Go concurrency: 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)
}
3

Concurrency Problems

// +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

fatal error: all goroutines are asleep - deadlock!

// 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!")
}
5

Runtime deadlock detection

6

Defeating runtime deadlock detection

// +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
    fmt.Println("Result is ", result)
}

This will be our running example

7

Static Analysis & Deadlock Detection by Global Graph Synthesis

8

Static Analysis & Deadlock Detection by Global Graph Synthesis

[1]: Honda, Yoshida, Carbone, Multiparty Asynchronous Session Types , POPL'08, J. ACM
9

The Multiparty Session Types (MPST) framework

[2]: Lange, Tuosto, Yoshida, From Communicating Machines to Graphical Choreographies , POPL'15
[3]: Brand, Zafiropulo, On communicating finite-state machines , J. ACM Vol. 30 No. 2, 1983
10

Type inference from Go code

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
    fmt.Println("Result is ", result)
}
11

Inferred local session types

Variable names: ch = main.t0, done = main.t1
12

Inferred Local Types to Goroutine Automata

13

Channel Automata

Note: Go channels valid regardless of the deadlock
14

Channel Automata

Channel Automata done & ch (only essential transitions)
15

Bonus: Select non-deterministic choice

// +build OMIT

package main

import (
	"fmt"
	"math/rand"
	"time"
)

func calc(ch chan int) {
	rand.Seed(time.Now().Unix())
	val := rand.Intn(5)
	time.Sleep(time.Duration(val) * time.Microsecond)
	ch <- val
}

func main() {
    ch1, ch2 := make(chan int), make(chan int)
    go calc(ch1)
    go calc(ch2)
    select {
    case ans := <-ch1:
        fmt.Println("Answer from ch1: ", ans)
    case ans := <-ch2:
        fmt.Println("Answer from ch2: ", ans)
    }
}
16

Global Graph Synthesis

17

Global Graph Synthesis: What is safe?

18

Fan-in pattern

// +build OMIT

package main

import (
	"fmt"
)

func work(out chan<- int) {
	for {
		out <- 42
	}
}
func fanin(input1, input2 <-chan int) <-chan int {
    c := make(chan int)
    go func() {
        for {
            select {
            case s := <-input1:
                c <- s
            case s := <-input2:
                c <- s
            }
        }
    }()
    return c
}

func main() {
	input1 := make(chan int)
	input2 := make(chan int)
	go work(input1)
	go work(input2)
	c := fanin(input1, input2)
	for {
		fmt.Println(<-c)
	}
}
19

Bigger example: htcat - Concurrent HTTP GETs

github.com:htcat/htcat (721 LoC)
20

Bigger example: htcat - Concurrent HTTP GETs

if err != nil {
    go cat.d.cancel(err)
    return
}
21

Conclusion

Static analysis tool

Synthesis tool (POPL'15 artifact)

22

Future Work

23

Thank you

Nicholas Ng & Nobuko Yoshida

Department of Computing

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