Understanding concurrency with behavioural types

Golang UK - 18 Aug 2017

Nicholas Ng

Imperial College London

Go and concurrency

Go is known for its built-in message-passing concurrency support

"Do not communicate by sharing memory; instead, share memory by communicating."

But does simple concurrency primitives make concurrency easy?

Go and concurrency

Simple concurrency primitives do not hide the complexity of concurrency

Concurrency opens up to a different class of bugs!

Concurrency problems

What can we do about them?

Go and concurrency

Artwork from gopherize.me / Ashley McNamara / Renee French

Go and concurrency

Go runtime deadlock detector

// +build ignore

package main

import (
	"fmt"
	"time"
)

func Gopher(speak chan<- string, listen <-chan string, done chan struct{}) {
    speak <- "Hey"
    fmt.Println("The other gopher said", <-listen)
    done <- struct{}{}
}

func main() {
    ch1, ch2 := make(chan string), make(chan string)
    done := make(chan struct{})
    // go makeCoffee() // What can go wrong?
    go Gopher(ch1, ch2, done) // Gopher 1 → ch1 → Gopher 2
    go Gopher(ch2, ch1, done) // Gopher 2 → ch2 → Gopher 1
    <-done
    <-done
}

func makeCoffee() {
	for {
		time.Sleep(1 * time.Second)
		fmt.Println("coffee brewing...")
	}
}

Detects deadlock when all goroutines are asleep

Ineffective if partially deadlocked: some goroutines are active

Deadlock detection

In short, runtime detector is not very robust (don't rely on it!)

Deadlock detection is harder than it seems

Maybe there are solutions in academic research?

Concurrency research

Deadlock detection is an important topic in concurrency research

Most research work listed uses Go, very few about Go

Understanding concurrency in Go

Our research aims to apply theoretical advances in concurrency

Communication deadlocks primer

Channel operations (send/receive) block when the channel is not ready for it

func main() {
    ch := make(chan int)
    <-ch // Nothing to receive, ch blocks, main sleeps.
}
func main() {
    ch2 := make(chan bool, 1)
    ch2 <- true // This is OK.
    // ch2 is now full.
    ch2 <- false // No buffer space in ch2, ch2 blocks, main sleeps.
}

When a channel operation blocks and has no chance of unblocking → deadlock

Observation

It does not matter what values are being sent and received
It is the behaviour of sending and receiving that directly causes deadlocks

Modelling concurrency

Process calculi: (e.g. CSP, CCS, π-calculus) family of models for concurrent processes

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)

Modelling concurrency

Process calculi vs. Go

Compare and contrast:

Essence of concurrency: Asynchronous π-calculus & Go

Behavioural Types

An abstract model of a Go program, only consists of its concurrent behaviours

A Behavioural Type model for a Go program

A framework for deadlock detection

Using Behavioural Types to detect deadlocks. Joint work with J. Lange, B. Toninho, N. Yoshida

Deadlock detection with Behavioural Types

Extract model from Go source code

Static analysis using Go's SSA Intermediate Representation (also used by guru etc.)

Convert into Behavioural Type model called MiGo

Deadlock detection with Behavioural Types

Use a model checker to check for properties in our model

Check for deadlocks and more on the MiGo model

e.g. Can a program always get to the end (without getting stuck/deadlock)?

Demo

The Dining Philosophers problem

The dining philosophers problem by Edsger Dijkstra

source: Benjamin D. Esham / Wikimedia Commons

Omitted details

"In theory, there is no difference between theory and practice. But, in practice, there is."
-- Jan L. A. van de Snepscheut

Concluding remarks

Further reading

Recent concurrency research on Go

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

↑ Summary in The Morning Paper by @adriancolyer
blog.coyler.org/2017/02/02/fencing-off-go-liveness-and-safety-for-channel-based-programming

Static Deadlock Detection for Go by Global Session Graph Synthesis (CC 2015)
N. Ng, N. Yoshida

Behavioural Types in Programming Languages [Book]
Foundations and Trends in Programming Languages, 2016
Ancona et al.

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