Go2Pins: Bridging the Gap between Model Checking and Software Verification

Description of this page

Go2Pins is a Golang-to-Golang transpiler. Its main objective is to bring verification techniques into the Golang realm.

This page summarizes how to install Go2Pins and details both the command line options and how to replay the benchmark presented in the paper

Downloading and running the Docker image

The easiest solution to experiment with Go2Pins is to run the docker image hosted by DockerHub. This docker also contains a copy of Spot, and LTSmin.

This docker image can be built locally using the GitHub public repository

Downloading DockerHub image can be done with the following command:

docker pull akaesus/go2pins
docker run --rm -it akaesus/go2pins

In this image, the /build/go2pins folder contains the Go2Pins tool.

cd /build/go2pins
make 
make check

Rebuilding Go2Pins from scratch

Alternatively, you can build Go2Pins on your own computer.

Requirements:

• Go >= 1.12
• Spot (development version)
• LTSmin
• clang (Note that you may want to use GCC but since we do not have a full integration with a build system, you will have to modify the generated Makefile by hand)

Then, simply follow the classical steps

git clone https://gitlab.lrde.epita.fr/spot/go2pins.git
cd go2pins
make
make check

You may want to replay a complete benchmark with

make benchmark

Playing with Go2Pins

Let us start our journey with Go2Pins with a small example, the concurrent computation of some fibonacci number. You can have a look to the tests/concurrent_fibonacci.go file.

Then just run the following command:

./go2pins -f -o output tests/concurrent_fibonacci.go
cd output
make

Note that:

• “-o output” specifies where all the files produced by Go2Pins will be stored
• “-f” indicates to erase the output directory if exist

This directory now contains a binary call ./go2pins-mc: this is the entry point of all the verification process. You can display all available options with

./go2pins-mc -help

Among the options of interest:

# Display the state-space in the DOT format
./go2pins-mc -display

# Only display the size of the state space
./go2pins-mc -kripke-size

# List all variables available for this model
./go2pins-mc -list-variables

# Check an LTL property with Spot or LTSmin backend. Note that 
# the syntax of these tools is different, we plan to write an automatic 
# translation tool so that it will be homogeneous
./go2pins-mc -ltl '[] "main_fibonacci_n==1"' --backend spot
./go2pins-mc -ltl '[] main_fibonacci_n == 1' --backend ltsmin

Benchmark Description and How to replay it!

Go2Pins embeds its benchmark inside of its git repository. As a consequence, you can simply run the following command. Nonetheless, notice that this benchmark uses a lot of memory. Consequently, trying to run this inside of the aforementionned Docker is discouraged: the memory limit and the nature of the Docker will slow down results and possibly fail due to the amount of memory required.

make benchmark

The benchmark is composed of two stages:

• The first one uses (huge) files coming from the RERS which have been translated into Go. This stage of the benchmark evaluates the scalability of our tool
• The second one evaluates the impact of Blackbox transitions by removing part of the state space

Please take a look to the benchs/run-benchmark.sh file to see more usage of Go2Pins options.

Limitations and Bug reports

Go2Pins is yet in development phase. Consequently, it has restrictions:

• Only 32-bit integer value types are currently supported.
• 32-bit integer array are supported, but raw initialisation is not fully supported, especially for local arrays
• Complex statements are not yet handled
• Function calls are authorized for goroutines, nonetheless they will be automatically considered as blackbox
• Unbounded channels are supported. But channels can only be declared
  as global variables

Ensuring that the input file respect all these limitation is very painful and we
prefer to put effort in supporting feature rather than detecting that we do not
support it. Nonetheless, we try to reject errors correctly, but, a lot of corner
cases are not yet covered. Please be indulgent, and bug report at
<renault [at] lrde . epita . fr>

Playing with LTLrec

Additionnaly, we offer an ltlrec binary. This binary aims to expand LTL formulae
(for checking recursive programs) with two keywords

• all: will develop an atomic proposition for every step of recursion
• any: will develop an atomic proposition for some step of recursion

This binary file is at the root of the projet. This binary is not yet fully integrated with go2pins since we aim to use it in other context (but integration is planned). Consequently, you have to list manually the names you want to expand through a JSON format. For instance the following command:

./ltlrec 'F all("a") || all("b")' '{"a": ["a1", "a2"], "b": ["b1", "b2", "b3"]}'

will replace all("a") by a conjunction of variables (here a1 and a2) while any("b") will perform a disjunction. The expected output is then

F ("a1" && "a2") || ("b1" && "b2" && "b3")