Go concurrency verification

The aim of this line of work is to verify channel-based concurrency interaction in Go using techniques from the research area of process calculi and type systems. This is a joint work with Bernardo Toninho (@bernpton), Julien Lange (@julienlange) and Nobuko Yoshida.

Tools

nickng/dingo-hunter is a static analyser for Go based on the go/ssa package from the Go project. The tool itself is designed to be an interface to Go programs, performing type inference/model extraction from Go code. Current analysis frontends include:

• Communicating Finite State Machines (CFSMs) modelling goroutines. This work was presented at Golang UK conference 2016 (video).
• A mini Go process calculi/type system (MiGo) as a high level, communication-only abstraction. This work was partly presented at Golang UK conference 2017 (video)

nickng/gospal is a new static analyser library for Go, also based on the go/ssa package from the Go project. It is a modular library that allows for analysis components to be reused. A context-sensitive MiGo inference tool migoinfer was built using the library which has better code coverage and error handling than the predecessor.

Publications

• Static Deadlock Detection for Concurrent Go by Global Session Graph Synthesis uses the CFSMs synthesis approach.
• Fencing off Go: Liveness and Safety for Channel-based Programming uses the MiGo approach.
• A Static Verification Framework for Message Passing in Go using Behavioural Types also uses the MiGo approach, but with an off-the-shelf model checker.