Static Deadlock Detection for Go by Global Session Graph Synthesis

Nicholas Ng

Imperial College London


Go is a programming language developed at Google, with channel-based concurrent features based on CSP. The Go runtime can detect global communication deadlocks when all threads of execution are blocked during execution, but deadlocks in other paths of execution could go undetected.
In this talk I will present a new static analyser for Go to find potential communication errors such as communication mismatch and deadlocks at compile time. The tool extracts the communication operations as session types, which are then converted into Communicating Finite State Machines (CFSMs). Finally, a recent theoretical result on choreography synthesis is applied to the CFSMs to generate a global graph representing the overall communication pattern of a concurrent program. If the synthesis is successful, then the program is free from communication errors.
The technique was implemented as a tool, and was applied to analyse common Go concurrency patterns and an open source application with over 700 lines of code.

Friday, September 16 2016