SRD: (Go) Static Race Detector #

A proof of concept work of extracting Structural Operational Semantics rules and applying it to do static race detection.

Structural Operational Semantics Rules #

$\textbf{Goroutine Creation}\ \frac{}{(G, M, C) \xrightarrow{\texttt{go f()}} (G \cup {\texttt{f()}}, M, C)}$

$\textbf{Memory Modification}\ \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{Channel Send}\ \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 Receive}\ \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{Print}\ \frac{\texttt{f()}\ \text{is}\ \texttt{fmt.Println(data)}}{(G, M, C) \xrightarrow{\texttt{go f()}} (G \cup {\texttt{f()}}, M, C)}$

Run #

Using Nix:

nix run nixpkgs#go -- run -race cmd/srd/main.go -- examples/example_*.go

Report #

nix shell nixpkgs#texlive.combined.scheme-full -c pdflatex docs/main.tex
nix shell nixpkgs#texlive.combined.scheme-full -c bibtex main.aux
nix shell nixpkgs#texlive.combined.scheme-full -c pdflatex docs/main.tex

License #

This repository content excluding all submodules is licensed under the MIT License, third-party code are subject to their original license.