Detecting Blocking Errors in Go Programs using Localized Abstract Interpretation

Oskar Haarklou Veileborg, Georgian-Vlad Saioc & Anders Møller, Aarhus University

Read the paper

To evaluate the proposed approach we developed the Goat tool that detects potential blocking errors in Go programs. The tool's source code is available at GitHub . Instructions and benchmark projects required for reproducing the results in the paper are available here.

In this example program:

package main

func main() {
	ch := make(chan int)
	go func() {
		ch <- 10
	}()

	go func() {
		ch <- 20
	}()

	<-ch
}

Goat detects that there is contention on the allocated channel, which makes either the first or second spawned goroutine block indefinitely. Warnings are issued for both lines with channel send operations. No warning is issued for the line containing the channel receive operation, as this operation will always synchronize with one of the two goroutines. Instructions for running the analysis on more programs is available together with the source code.

Contact {oskar,gvsaioc,amoeller}@cs.au.dk if you experience issues with, or have questions about the tool.