Something went wrong. Try again.
srd: (go) static race detector
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205\documentclass[12pt]{article}\parindent=0pt
\usepackage[utf8]{inputenc}\usepackage[margin=1in]{geometry}\usepackage{setspace}\doublespacing
\usepackage{amsmath}\usepackage{mathtools}\usepackage[inline]{enumitem}\usepackage[pdftex]{hyperref}\usepackage{xurl}\usepackage{orcidlink}
\usepackage{color}\usepackage{xcolor}\definecolor{LightGray}{gray}{0.9}\usepackage{minted}
\title{Exploring Go's Data Race Detection}\author{Yifei Sun\orcidlink{0000-0002-1591-7458}\\\texttt{yifei.sun@utah.edu}}\date{May 11, 2023}
\begin{document}
\maketitle
\begin{abstract}Go has become an increasingly popular programming language, large companies have started using it for critical components in their production systems. However, as a language designed for concurrent programming and with easy access to spawn light-weight threads, even experienced developers can write code with race conditions hidden deep within, making the debugging process time consuming and challenging. The built-in race detection tool in Go may increase memory usage by 5-10x and slow down execution by 2-20x \cite{godev-golang-runtime-race-detector}, and as a dynamic data race detector, it can provide relevant warning messages only at runtime. In this project \footnote{GitHub: \url{https://github.com/StepBroBD/SRD}.}, we are exploring the possibilities of running static analysis on Go source code to achieve race detection and provide useful diagnostic information to developers similar to Go's built-in data race detector with relatively low false positive and false negative rate.\end{abstract}
\section{Introduction}
In the realm of concurrent programming languages, Go stands apart with its unique approach to managing communication between concurrently executing processes. The philosophy of Go is encapsulated in the slogan: ``Do not communicate by sharing memory; instead, share memory by communicating." \cite{godev-effective-go}, this central tenet underpins the design of Go's concurrency features, with channels at its heart. However, like any powerful tool, Go's channels feature is not immune to misuse. A common area of misunderstanding is the proper use of channels in conjunction with goroutines, for example, knowing when to close channels and ensuring that goroutines do not leak by failing to receive from them. Misuse of these features can lead to runtime panics or goroutine leaks, both of which can be problematic in a production environment. Through this project, we hope to demystify these complexities and formalize the correct usage of Go's channels and goroutines using structural operational semantics (SOS) and integrating SOS rules into static analysis tools.
\section{Related Work}
% Type-Based Race Detection for Java: https://www.cs.cornell.edu/courses/cs711/2005fa/papers/ff-pldi00.pdf
\textbf{\textit{Type-Based Race Detection for Java}} \cite{type-based-static-analysis-for-race-detection}:The main idea of this paper is to present a static race detection analysis for multithreaded Java programs based on a formal type system that captures many common synchronization patterns. The paper describes the implementation of this system, called rccjava, and demonstrates its effectiveness in eliminating race conditions by checking over 40,000 lines of Java code. The authors also discuss the benefits of using this type system, including early detection of race conditions and improved documentation of locking strategies used by the program.
While the paper specifically focuses on Java programs, the ideas presented in the paper can be applied to other statically typed languages, including Go. It's possible to use similar approach mentioned in the paper to build a race detector that tracks shared variables and checks that they are accessed safely by multiple go routines. It also requires additional annotations to be added to the code to help identify shared variables and synchronization points.
The type system presented in this paper works by tracking the protecting lock for each shared field in a Java program and verifying that the appropriate lock is held whenever a shared field is accessed. This is done through a set of rules that are added to Java's type system, which allow the type checker to reason about the locking discipline used by the program. The type system also requires additional type annotations to be added to the code, which help identify shared variables and synchronization points. These annotations are used by the type checker to ensure that shared variables are only accessed while the appropriate lock is held.
% An Operational Semantic Basis for OpenMP Race Analysis: https://arxiv.org/pdf/1709.04551.pdf
\textbf{An Operational Semantic Basis for OpenMP Race Analysis} \cite{openmp-operational-semantics}:This paper presents an operational semantics for OpenMP that models the concurrency structure of OpenMP and enables data race detection for structured parallelism. The authors argue that their approach can help researchers and tool developers better understand OpenMP concurrency, and build more precise data race checkers that reduce memory overheads.
One key idea from the paper that could be applied to Go's data race checking is the use of an operational semantics to model concurrency structures. Other ideas from the paper that could be applicable to Go's data race checking include using state machines to implement operational semantics rules, defining conventions for operational semantics rules, and modeling language constructs in a concurrency model.
% Operational Semantics for Multi-Language Programs: https://users.cs.northwestern.edu/~robby/pubs/papers/popl2007-mf-color.pdf
\textbf{Operational Semantics for Multi-Language Programs} \cite{operational-semantics-for-multi-language}: This paper takes a step towards higher-level models of interoperating systems by abstracting away low-level details of interoperability and focusing on semantic properties like type-safety and observable equivalence. The authors also discuss related work in this area, including formalisms for the semantics of COM and a type-safe intermediate language designed specifically for multi-language interoperation.
% Other resources:% Go Language Patterns: http://www.golangpatterns.info% Go Concurrency Patterns: https://go.dev/talks/2012/concurrency.slide#1% Advanced Go Concurrency Patterns: https://go.dev/talks/2013/advconc.slide#1% Pipelines and Cancellation: https://go.dev/blog/pipelines
\textbf{Other Resources}:In addition to these academic resources, several practical resources provide valuable insights into structural operational semantics and the patterns/practices of Go. These include:\begin{enumerate*}\item ``Operational Semantics" (\url{https://cs.lmu.edu/~ray/notes/opsem/}),\item ``Go Language Patterns" (\url{http://golangpatterns.info}),\item ``Go Concurrency Patterns" (\url{https://go.dev/talks/2012/concurrency.slide}),\item ``Advanced Go Concurrency Patterns" \url{https://go.dev/talks/2013/advconc.slide}), and\item ``Pipelines and Cancellation" (\url{https://go.dev/blog/pipelines}).\end{enumerate*}These resources offer a wealth of practical examples and best practices that complement the theoretical foundations presented in the academic literature.
\section{Problem}
A common misuse of Go's channels and goroutines that can lead to data races involves the incorrect assumption that sending to or receiving from a channel implies synchronization between goroutines.
\begin{figure}[!ht]\begin{minipage}[c]{0.45\linewidth}\begin{minted}[frame=lines,framesep=1mm,baselinestretch=1,bgcolor=LightGray,fontsize=\footnotesize,linenos=true,autogobble=true,]{go}package main
import "fmt"
func main() { var data int
go func() { data++ }()
go func() { fmt.Println(data) }()}\end{minted}\caption{Example of a data race caused by unsynchronized access to shared data across multiple goroutines.}\label{fig:ex1}\end{minipage}\hfill\begin{minipage}[c]{0.45\linewidth}\begin{minted}[frame=lines,framesep=1mm,baselinestretch=1,bgcolor=LightGray,fontsize=\footnotesize,linenos=true,autogobble=true,]{go}package main
import "fmt"
func main() { var data int done := make(chan bool)
go func() { data++ done <- true }()
go func() { <-done fmt.Println(data) }()}\end{minted}\caption{Corrected version of Figure 1 using channels to synchronize goroutines and prevent data races.}\label{fig:ex2}\end{minipage}\end{figure}
In Figure \ref{fig:ex1}, two goroutines are spawned. One increments the global data variable, and the other attempts to print the data variable. However, there is no guarantee of the order in which these goroutines will be scheduled to run. As a result, the printed value could be 0 (if the printing happens before the increment) or 1 (if the printing happens after the increment). This is a classic example of a data race. The idiomatic Go solution to this problem is to use channels to synchronize the goroutines. The sending goroutine can send a signal over the channel when it has finished its operation, and the receiving goroutine can wait for this signal before it begins its operation. In the corrected code (Figure \ref{fig:ex2}), a \texttt{done} channel is used to synchronize the two goroutines. The incrementing goroutine sends \texttt{true} over the \texttt{done} when it has finished its operation. The printing goroutine waits to receive from the \texttt{done} before it begins its operation, ensuring that it only prints \texttt{data} after the incrementing goroutine has finished.
This use of channels to synchronize goroutines is in line with the Go philosophy of sharing memory by communicating, rather than communicating by sharing memory. Instead of both goroutines accessing the shared data variable with no synchronization (which leads to a data race), the goroutines use a channel to communicate and synchronize their operations, ensuring that the data variable is only accessed when it is safe to do so.
\section{Structural Operational Semantics}
To formalize the problem and above mentioned fix, we can represent the program as a set of rules that describe how the state of the system changes based on certain conditions. In this case, we want to model the behavior of goroutines and channels in Go, particularly focusing on the synchronization of goroutines via channels.
The configuration of our program can be defined as a tuple $(G, M, C)$ where:
\begin{itemize} \item $G$ is the set of goroutines, \item $M$ is the memory, represented as a mapping from variables to values, \item $C$ is the set of channels, represented as a mapping from channel identifiers to lists of values.\end{itemize}
We can use the following SOS rules:
\begin{align*}& \frac{}{(G, M, C) \xrightarrow{\texttt{go f()}} (G \cup \{\texttt{f()}\}, M, C)} & \textbf{Goroutine Creation} \\\vspace{2.5mm}\\& \frac{\texttt{f()}\ \text{is}\ \texttt{data++}}{(G, M, C) \xrightarrow{\texttt{go f()}} (G - \{\texttt{f()}\}, M[\texttt{data} \rightarrow M(\texttt{data}) + 1], C)} & \textbf{Memory Modification}\\\vspace{2.5mm}\\& \frac{\texttt{f()}\ \text{is}\ \texttt{done <- true}}{(G, M, C) \xrightarrow{\texttt{go f()}} (G - \{\texttt{f()}\}, M, C[\texttt{done} \rightarrow C(\texttt{done}) \cup \{\texttt{true}\}])} & \textbf{Channel Send}\\\vspace{2.5mm}\\& \frac{\texttt{f()}\ \text{is}\ \texttt{<-done}}{(G, M, C) \xrightarrow{\texttt{go f()}} (G - \{\texttt{f()}\}, M, C[\texttt{done} \rightarrow C(\texttt{done}) - \{\texttt{true}\}])} & \textbf{Channel Receive}\\\vspace{2.5mm}\\& \frac{\texttt{f()}\ \text{is}\ \texttt{fmt.Println(data)}}{(G, M, C) \xrightarrow{\texttt{go f()}} (G \cup \{\texttt{f()}\}, M, C)} & \textbf{Print}\end{align*}
Please note that this is a simplified model. In a more comprehensive model, you would want to handle cases like sending to a full channel, receiving from an empty channel, and more complicated goroutine interactions. In addition, you might want to include a scheduler in the state to control the order in which goroutines are run, and to handle the non-deterministic scheduling of goroutines by the Go runtime.
\section{Static Analysis}
Accompanying this report, there is a demo Go program that usessimple static analysis technique to detect potential data races. The analysis is performed based on the traversal of the Abstract Syntax Tree (AST) of given Go code specified by a command line argument.
The main structures are:
\begin{itemize} \item The State struct, which models the state of a Go program in terms of active goroutines, memory locations that have been written to, and channels that have been used for sending and receiving data. \item The Visitor struct, which is used for traversing the AST. It updates the State according to the different types of nodes encountered in the AST.\end{itemize}
The analysis checks for potential data races by looking for memory locations that have been written to more than once, which could indicate a data race if these write operations are not properly synchronized.
However, it's important to note that this analysis is a simple and somewhat naive approach to data race detection. It has several limitations and assumptions that may lead to inaccuracies:
\begin{enumerate} \item All function calls are assumed to be print statements, which simplifies the analysis but is not accurate for general Go code. \item The analysis assumes that every increment/decrement operation indicates a write to a shared memory location. However, in real Go programs, many of these operations might be operating on local variables that are not shared between goroutines. \item The analysis doesn't account for the synchronization provided by Go's concurrency primitives like locks or the proper use of channels.\end{enumerate}
To make this program a reliable tool for data race detection, it would need to be significantly expanded and refined to accurately model the behavior of Go programs, including the semantics of Go's concurrency primitives and the scope and lifetime of variables. The goroutine creation and memory modification rules would need to be more precisely defined and applied only in appropriate contexts. In its current form, it serves as a basic demonstration of how AST traversal can be used for static analysis.
\nocite{*}\bibliographystyle{alpha}\bibliography{references.bib}
\end{document}