Static Deadlock Detection for Go by Global Session Graph Synthesis

Nicholas Ng

Imperial College London

Motivation: Go and Concurrency

Work previously presented at CC 2016 and Golang UK 2016

2

This talk

3

Concurrency in Go

" Do not communicate by sharing memory; instead, share memory by communicating. "
-- Go language proverb

4

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)
}
5

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)
}
6

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

Runtime deadlock detection

8

Go runtime deadlock detector

If we add a benign, long-running goroutine..

// +build OMIT

package main

import (
	"fmt"
	"time"
)

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

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

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

    deepThought(ch)
    answer := <-ch 
    fmt.Printf("The answer is %d\n", answer)
}

// END OMIT

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

9

Static Analysis & Deadlock Detection by Global Graph Synthesis

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

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
11

Type inference from Go code

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()
12

Type inference from Go code

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)
    }
}
13

Compose and synthesise global graph

Session types obtained from all goroutines in program

Next: Convert to Communicating Automata

14

Local Session Types as Communicating Automata

15

Global Graph Synthesis

16

Global Graph Synthesis: What is safe?

17

Global Graph Synthesis: In conclusion

Incompatible: this is not a well formed global graph

18

Bigger example: htcat - Concurrent HTTP GETs

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

Bigger example: htcat - Concurrent HTTP GETs

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

Conclusion

Static analysis tool

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

Synthesis tool (POPL'15 artifact)

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

21

Ongoing related work

📄 Fencing off Go: Liveness and Safety for Channel-based Programming
J. Lange, N. Ng, B. Toninho, N. Yoshida, POPL 2017

We'll update at next ABCD meeting

22

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