GCatch contains a suite of static detectors aiming to identify concurrency bugs in large, real Go software systems. Concurrency bugs covered by the current version of GCatch include blocking misuse-of-channel (BMOC) bugs, deadlocks caused by misuse of mutexes (\eg, lock-with-unlock, double lock), races on struct fields, and races due to errors when using the testing package. The technical details of GCatch are presented in Section 3 of our ASPLOS paper [1].
GCatch leverages Z3 for constraint solving. If you have already installed Z3, you can use the install.sh
script is to install GCatch. You can also install Z3 together with GCatch using the installZ3.sh
script.
After the installation, you can run the run.sh
script to execute GCatch on a buggy version of gRPC.
-
Directory
analysis
contains static analysis routines shared by multiple checkers (e.g., computing post-dominator). -
Directory
checkers
contains code for implementing the checking functionalities. -
Directory
cmd
is the entry point of GCatch. -
Directory
config
contains configuration files of GCatch. -
Directory
instinfo
contains code for analyzing Go SSA instructions. -
Directory
output
contains code for printing the detection results. -
Directory
path
contains code for computation conducted on CFG. -
Directory
ssabuild
contains code for transforming input programs into SSA. -
Directory
syncgraph
contains code for interaction with call graph, alias analysis, and Z3. -
Directory
testdata
contains a buggy version of gRPC. -
Directory
tests
contains toy programs to test traditional checkers. -
Directory
tools
contains copies of external packages. -
Directory
util
contains utility code shared by different components of GCatch.
Please refer to the demonstration scripts to figure out how to use GCatch’s code.
[1] Ziheng Liu, Shuofei Zhu, Boqin Qin, Hao Chen and Linhai Song. “Automatically Detecting and Fixing Concurrency Bugs in Go Software Systems.” In ASPLOS’2020.