Static Trace-Based Deadlock Analysis for Synchronous Mini-Go

TL;DR

This paper presents a static analysis method for detecting deadlocks in Go programs that use synchronous channels, employing automata-based techniques to analyze communication traces and ensure deadlock-freedom.

Contribution

It introduces a novel automata-based approach using extended regular expressions with forks to analyze communication traces for deadlock detection in Go programs.

Findings

Effective deadlock detection demonstrated on example programs

Automata-based analysis can identify deadlocks accurately

Method is implemented and evaluated successfully

Abstract

We consider the problem of static deadlock detection for programs in the Go programming language which make use of synchronous channel communications. In our analysis, regular expressions extended with a fork operator capture the communication behavior of a program. Starting from a simple criterion that characterizes traces of deadlock-free programs, we develop automata-based methods to check for deadlock-freedom. The approach is implemented and evaluated with a series of examples.