Fencing off Go Applied - A Practical Look at a Go Research Paper

Fencing off Go: Liveness and safety for channel-based programming, Lange et al., POPL 2017.

In Go 1.8, the following holds true:

Go can only detect global deadlocks at runtime, but provides no compile-time protection against all too common communication mismatches or partial deadlocks.

In this paper we are presented with a work that:

[...] develops a static verification framework for bounded liveness and safety in Go programs, able to detect communication errors and partial deadlocks in a general class of realistic concurrent programs, including those with dynamic channel creation and infinite recursion.

The paper introduces MiGo, a process calculus that models a subset of concurrency features in Go. The MiGo language is extended with concurrent behavioural types.

The work has also produced a tool-chain that implements the framework. It can analyse original Go source code and transform it into MiGo, with no need to annotate existing code.

The tool-chain is composed by two parts, dingo-hunter (dubbed GoInfer in the paper) and Gong.

The program dingo-hunter converts a Go program to MiGo and infers concurrent behavioural types. The resulting MiGo program is analysed by Gong which checks for liveness and channel safety.

The liveness check detects partial deadlocks by verifying that channel-based communication will always eventually execute.

The channel safety check detects communication errors by verifying that the program does not send to or close a closed channel, both of which will cause a run-time panic in Go.

Channel Safety

A trivial example of a program where we have introduced a channel safety error:

package main

func main() {
    ch := make(chan struct{})
    close(ch)
    close(ch)
}

Closing the channel more than once causes a run-time panic in Go.

Running dingo-hunter migo on the Go program outputs a MiGo program:

def main.main():
    let t0 = newchan main.main.t0_0_0, 0;
    close t0;
    close t0;

Running Gong on the MiGo program informs us that the program is not safe:

Bound (k): 1
Number of k-states: 3
Liveness: True
Safety: False

In Gong's debug output, we can see the reachable states and the unsafe term:

Bound (k): 1
Number of k-states: 3

[Debug]k-reachable states:
new -1 t0.((t0:B:0K:0))
new -1 t0.(close t0;0 | (t0:B:0K:0))
new -1 t0.(close t0;close t0;0 | [t0:B:0K:0])

Liveness: True
Safety: Gong: Term not safe: ["close t05;close t05;0","[t05:B:0K:0]"]

Liveness

A trivial example of a program where we have introduced a channel deadlock:

package main

func main() {
    ch := make(chan struct{})
    <-ch
}

The receive operation will block forever because a value will never be available.

Running dingo-hunter migo on the Go program outputs a MiGo program:

def main.main():
    let t0 = newchan main.main.t0_0_0, 0;
    recv t0;

In Gong's debug output, we are presented with the reachable states and a term that is not live:

Bound (k): 1
Number of k-states: 1

[Debug]k-reachable states:
new -1 t0.(t0?;0 | [t0:B:0K:0])

Liveness: Gong: Term not live: ["t01?;0","[t01:B:0K:0]"]

Future Work

The tool-chain is useful in its current state.

With improved tooling to make the output easier to interpret and reduce its analysis time1, it would make a nice addition to a Go programmers' workflow.

Furthermore, the authors have planned to extend their work to:

[...] account for channel passing, and also lock-based concurrency control, enabling us to verify all forms of concurrency present in Go.


  1. It takes more than 10 minutes to analyse a 48 lines of code implementation of the dining philosophers problem on a modest machine.