π-calculus, Session Types research at Imperial College
Godel2 is a model checker for MiGo types that returns results of
liveness and safety checks for channels and mutex locks, as well as
the presence of data races on shared pointers.
Below are instructions to try the tool-chain, which was developed for Static Race Detection and Mutex Safety and Liveness for Go Programs and has passed the ECOOP 2020 Artifact Evaluation.
The artifact is a tool-chain and set of examples we used to evaluate our approach, described in Section 8 of the paper. All of the example inputs are Go program source code. We infer their MiGo types, then verify their liveness and safety following the theoretical results presented in the paper. The purpose of this page is to give instructions to reproduce the results of Table 1 (page 24). The tool-chain consists of two separate tools:
The examples we used can be found in a dedicated repository. Additionally, we give instructions to test your own examples. You can write your own Go programs and feed them into MiGoInfer+ then Godel2 (see limitations). Alternatively, you can write MiGo types directly and check them with Godel2.
The inference tool is a prototype, and does not cover all syntax of the Go programming language. In particular, we have no support for dynamically spawning new threads and channel in unbounded (or input dependent) loops. As part of the infrastructure, some extra tools are built to help with troubleshooting in the case of inference error.
Below are instructions to run the artifact, using pre-compiled binaries (for any architecture able to run Docker with at least 2GB of available RAM and 2GB of available disk space). Alternatively, one can find the instructions to compile their own versions of the tools in their respective repositories.
First, make sure you have Docker Desktop installed and running on your system.
Second, pull our pre-built Docker image.
docker pull jgabet/godel2
This image contains pre-compiled binaries for MiGoInfer+ and Godel2.
Our examples can be downloaded and run from our benchmark repository.
The repository contains a convenience script, run.sh,
to run all of the provided examples (including a warning and prompt
before running the two more time-consuming ones).
The results obtained from running the tools should correspond with the
results in the paper and the ones in the above repository’s README.
Alternatively, one can run their own examples using the Docker command line, as explained in Godel2’s source repository, like so:
Infer MiGo types from Go source code:
cd /path/to/example
docker run -ti --rm -v $(pwd):/root jgabet/godel2:latest migoinfer example.go > example.cgo
Model-check MiGo types:
cd /path/to/example
docker run -ti --rm -v $(pwd):/root jgabet/godel2:latest Godel example.cgo # Model check
docker run -ti --rm -v $(pwd):/root jgabet/godel2:latest Godel -T example.cgo # Termination check
We thank Nicholas Ng for his initial help in developing the tool, and David Castro-Perez and Fangyi Zhou for their comments and testing.