go2pins

README

Go2Pins: Bridging the Gap between Model Checking and Software Verification

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

Usage

Go2Pins is itself a Go program. As such, you will need to have installed a distribution of Go on your computer in order to build it.

The minimum recommended Go version is 1.12.

Once you have cloned the repository:

cd go2pins

# Build go2pins and run tests
make 
make check

# Then, you can feed your program to go2pins
./go2pins -o output tests/concurrent_fibonacci.go

# The output directory will contain all the files necessary to compile the
# shared library respecting the PINS interface
cd output
make

# Then, you can  generate the state tree of your program.
# Note that this is only aivalable if you have Spot's modelcheck
# utility in your PATH (in <spot>/tests/ltsmin/modelcheck)
./go2pins-mc -display

# You can also perform LTL model checking by running either 
./go2pins-mc  '<some_ltl_formula>' -backend spot

# or if you have LTSmin backend installed
./go2pins-mc  '<some_ltl_formula>' -backend ltsmin

# Note that the LTL syntax may differ according to the various backend.
# Spot requires escaping while ltsmin refuses uppercase atomic propositions
# and requires spaces
#   - Spot syntax:      '[] "main_fibonacci_n==1"'
#   - LTsmin syntax:    '[] main_fibonacci_n == 1' 

# The list of available commands is accessible through
./go2pins-mc -help

Performances

You can run the benchmark associated to this tool by running

make benchmark

Nonetheless, even with 8 threads and 200Go of RAM this benchmakr will take at least multiple day. Consequently You can run the benchmark on small problems by running

make demo

Note that some part of this benchmark requires a lot of memory and can then fail on your machine.

LTLrec

A tool named ltlrec is provided when running make. This tool implements the LTLrec sugaring useful for handling recursion. For now, this tool is external so that it can easily be used by other tools. We plan to integrate this tool directly to Go2Pins.

As a consequence, the equivalences must be specified by hand though a JSON file. For instance:

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

will output

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

Our goal is to integrate this tool directly inside of the output directory.

Limitations

• 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 for loop 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. We try to reject it correctly, but, a lot of corner cases are not covered. Please be indulgent, and bug report.

Architecture of the project

• main.go is the entry point of the program. It takes care of argument parsing, file parsing and any kind of top-level transformation and templating logic.
• src/decl/ is a utility library to quickly generate the AST representation of Go types and values.
• src/transform/ contains the logic of all other transformations.
• tests/ contains example programs that can be fed into go2pins.
• tools/ contains utility tools to inspect the AST of Go programs. They should be built separately.
• boilerplate/ contains all the boilerplate necessary to create a PINS shared library with cgo.
• cspinfo information about concurrency
• benchs the benchmark of the paper