Towards Bug-Free Distributed Go Programs

TL;DR

This paper presents a verification framework for proving the absence of communication races in distributed Go programs, enhancing reliability by static analysis of message passing synchronization.

Contribution

It introduces a static verification method specifically designed for distributed Go programs that use message passing, addressing communication races.

Findings

Framework can prove absence of communication races

Handles buffered and unbuffered channels

Applicable to subset of Go language

Abstract

Programmers of distributed systems need to reason about concurrency to avoid races. However, reasoning about concurrency is difficult, and unexpected races show up as bugs. Data race detection in shared memory systems is well-studied (dynamic data race detection [13], behavioral types [15], dynamic race detection [31]). Similar to how a data race consists of reads and writes not related by happens-before at a shared memory location, a communication race consists of receives and sends not related by happens-before on a shared channel. Communication races are problematic: a receiver expects a specific message from a specific sender, but with a communication race, the receiver can receive a message meant for another receiver, or not receive anything at all. In this work, we describe a verification framework that can prove the absence of communication races for distributed programs that use a subset of the Go programming language, where synchronization is mainly achieved via message passing. We statically reason about how a distributed program executes, using a happens-before order, extended to buffered and unbuffered channels.