MobilityReadingGroup

Gong

Channel Liveness and Safety checker

Gong is a liveness and safety checker for MiGo types.

Table of Contents

• Overview of artifact
• Instructions
  • Option 1: Use pre-compiled binaries
  • Option 2: Build from source
• Running the artifact
• Writing your own tests
• References
• Demo interface

Overview of artifact

The artifact is a tool-chain and set of examples we used to evaluate our approach, described in Section 7 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 table below describes the examples we evaluated in the paper and (if applicable) their origins. The purpose of this page is to give instructions to reproduce the results of Table 1 (page 11). The tool-chain consists of two separate tools:

1. GoInfer takes a Go program source code as input and infer its MiGo type; and
2. Gong verifies liveness and safety properties of a MiGo type

The table below describes the examples we evaluated in the paper and (if applicable) their origins. Additionally, we give instructions to test your own examples. You can write your own Go programs and feed them into GoInfer then Gong (see limitations). Alternatively, you can write MiGo types directly and check them with Gong.

Notes on limitations

The inference tool is an early prototype, and does not cover all syntax of the Go programming language. In particular, we have limited support for closures, and functions with no communication are best inlined. As part of the infrastructure, some extra tools are built to help with troubleshooting in the case of inference error.

Examples in paper

Instructions

Below are instructions to run the artifact, there are two options:

Most instructions assume 64-bit x86-64 Ubuntu Linux, and uses bash as shell. (for example export PATH=$PATH:... would be setenv PATH $PATH:... in a csh-based shell)

• Use pre-compiled binaries (for 64-bit Linux on x86-64 architecture)
• Build from source

Step 1a: Use pre-compiled binaries for Linux

Note Below pre-compiled binaries are for for Linux x86-64 only.

First, download and unpack tools.zip. The md5sum of the zip archive is 1a0c8f2b1268184bbc3aaddd13d7f65a, and contains two executables, dingo-hunter and Gong, and the examples in the paper with the scripts to run them.

unzip tools.zip # extracts to popl17-examples/

Next, download the latest version of the Go tool chain in the go1.7 branch. As of writing the current version is go1.7.1. It is strongly recommended to use the binary package provided at golang.org and install to /usr/local rather than distro-packaged version.

Follow the installation instructions of the Go toolchain.

Once the Go toolchain is installed, check that the go command is available in your $PATH and the version of Go is correct:

go version
go version go1.7.1 linux/amd64

Check that the $GOPATH environment variable is configured correctly, run the following and check that the GOPATH is recognised and set to a directory (e.g. $HOME/work).

go env
GOARCH="amd64"
GOBIN=""
GOEXE=""
GOHOSTARCH="amd64"
GOHOSTOS="linux"
GOOS="linux"
GOPATH="/home/nickng/work"
GORACE=""
GOROOT="/usr/local/go"
GOTOOLDIR="/usr/local/go/pkg/tool/linux_amd64"
CC="gcc"
CXX="g++"
CGO_ENABLED="1"

Finally, follow the instructions in the Running section to test the artifacts.

Step 1b: Build from source

The instructions below will install the software and package dependencies for building from source.

• ghc 7.10.1+, with following packages via cabal.
  • ansi-terminal
  • unbound
  • cmdargs
  • parsec
  • parallel
• go1.7.1 binary package, package dependencies for Go packages are automatically installed by go get (see Installing Go and source dependencies below)

The instructions have been tested on a 64-bit Ubuntu Linux (amd64).

Installing Go and source dependencies

Download the latest version of the Go tool chain in the go1.7 branch. As of writing the current version is go1.7.1. It is strongly recommended to use the binary package provided at golang.org and install to /usr/local rather than distro-packaged version.

Follow the installation instructions of the Go toolchain.

Once the Go toolchain is installed, check that the go command is available in your $PATH and the version of Go is correct:

go version
go version go1.7.1 linux/amd64

Check that the $GOPATH environment variable is configured correctly, run the following and check that the GOPATH is recognised and set to a directory (e.g. $HOME/work).

go env
GOARCH="amd64"
GOBIN=""
GOEXE=""
GOHOSTARCH="amd64"
GOHOSTOS="linux"
GOOS="linux"
GOPATH="/home/nickng/work"
GORACE=""
GOROOT="/usr/local/go"
GOTOOLDIR="/usr/local/go/pkg/tool/linux_amd64"
CC="gcc"
CXX="g++"
CGO_ENABLED="1"

To install the package dependencies of the tool use the go get command to download, build and install the package from source code. go get command to download, build and install the package from source code. The parameter -u is for update and -v is for verbose which displays what is being downloaded:

go get -u -v github.com/nickng/dingo-hunter

Dependencies for Go is automatically resolved, and the binary dingo-hunter will be installed in $GOPATH/bin

Installing Haskell

Install the Haskell Platform from your OS (e.g. via apt-get on Debian/Ubuntu Linux, or download directly from haskell.org). As of writing the current version of ghc in Ubuntu 16.04 is 7.10.3 which is the version we have tested these installation instructions on.

sudo apt-get install haskell-platform

Install the dependencies with cabal:

cabal update

cabal install ansi-terminal unbound cmdargs parsec parallel

Compiling the artifact tools

GoInfer The GoInfer tool (dingo-hunter) is already installed from the go get command above.

Gong The Gong tool source code can be downloaded from GitHub as a zip archive.

unzip gong-master.zip

Build the tool by running ghc on Gong.hs, which compiles the as a binary named Gong.

cd gong-master; ghc Gong.hs

Then add the directory containing the Gong binary to your PATH. This is needed for our verify script to find the tool.

export PATH=$PATH:$(pwd)

Finally, download and unzip examples.zip. The md5sum the zip archive is 8c23e1f8881c015298fdebc1fcae3a70, and contains examples in the paper with scripts to run them.

unzip examples.zip # extracts to popl17-examples/

docker run nickng/gong:popl17ae Gong -A path/to/file.migo

alias Gong='docker run nickng/gong:popl17ae Gong'

Step 2: Running the artifact

Make sure that both the dingo-hunter and Gong tool are installed and available in the path. Follow the instructions below to run the artifact.

To run the tool, we provide a wrapper shell script verify to run all the components for all the examples listed in our examples.

In the popl17-examples/ directory, use the verifyall script to run all of the examples at once.

./verifyall

Alternatively, we provide a verify script to run individual examples, for example, to run the fib example:

./verify fib

The script executes two statically compiled binary for 64-bit Ubuntu Linux (amd64). First it runs the dingo-hunter tool (referred to as the GoInfer tool in the paper) to extract MiGo types from given source code. The inferred MiGo types are then passed to the Gong tool to check for liveness and safety.

For clarity we use the .migo extension below for inferred MiGo types file, but the content is plain text.

To run the individual tools separately, first infer a .migo file from a given input Go source code, for example:
The --no-logging parameter suppresses the inference logging output, see also logging.

dingo-hunter infer path/to/source.go --no-logging --output inferred.migo

Then run the Gong tool to check the inferred inferred.migo file, which will output in the format similar to below:

Gong -A inferred.migo
Bound (k): 2
Number of k-states: 4
Liveness: True
Safety: True

The results obtained from running the tools should correspond with the results in the paper (see table).

Writing your own tests

You can write your own tests for the tools, dingo-hunter accepts as input source code with a main() function. Below is an example of a simple send/receive between two goroutines.

You can use the online webservice Go Playground to execute Go code, or to check that the code has valid syntax. For example, here.

package main

import "fmt"

func main() {            // main() function is the program entry point
    ch := make(chan int) // Initialise an unbuffered integer channel 'ch'
    go sender(ch)        // Spawn a goroutine with 'sender' function with 'ch' as argument
    fmt.Println(<-ch)    // Receive from channel 'ch', then print received value to stdout
}
func sender(ch chan int) {
    ch <- 42             // Send value '42' to channel 'ch'
}

Save the above content as main.go and run the following to convert it into MiGo types format.

dingo-hunter infer main.go

You can also manually write a MiGo type for the above program. The equivalent MiGo types are given as follows:

def main.main():
    let ch = newchan int, 0; # This creates a new channel 'ch', buffer size 0
    spawn sender(ch);        # Spawn the sender def as a thread, with 'ch' as parameter
    recv ch;                 # Receive from channel 'ch'
def sender(ch):
    send ch;                 # Send to channel 'ch'

Save the above content as main.migo and use Gong to check it:

Gong -A main.migo

MiGo types inferred from the paper examples can be found in popl17-examples/out/, and you can find additional MiGo type examples in this zip archive.

Demo interface

A demo interface was developed for the tool (screenshot below). To use the demo interface, switch to the master branch:

git checkout master

Then run the dingo-hunter tool with the serve command, and visit 127.0.0.1:6060:

go run main.go serve # Runs http server on port :6060

Alternative it’s possible to use go install to permanently replace the currently installed dingo-hunter binary with the master branch version (in $GOPATH/bin):

go install; \
dingo-hunter serve # runs an HTTP server on port :6060

References

[GKL2014] E. Giachino, N. Kobayashi, and C. Laneve. Deadlock analysis of unbounded process networks. In CONCUR, volume 8704 of LNCS, pages 63-77. Springer, 2014

[NY2016] N. Ng and N. Yoshida. Static Deadlock Detection for Con-current Go by Global Session Graph Synthesis. In CC 2016,pages 174-184. ACM, 2016

[M1989] R. Milner. Communication and Concurrency. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1989

Troubleshooting

This section is intended for developers who encounter problems when inferring from a new piece of source code but our tools could not give a satisfactory output.

View SSA To view the SSA form of the source code analysed, this command outputs the SSA input used as input for the analyses. This is similar to ssadump but is configured to use the same options and configurations as the inference.

dingo-hunter buildssa --dump /path/to/source.go

From the generated SSA user can see the instructions and registers for each function and see the correspondence between the SSA and the inferred MiGo types.

Logging By default, running the inference outputs an analysis log to stdout. To write the log to a different location, use the --log file.log parameter:

dingo-hunter infer --log source.log /path/to/source.go

View reachable states To view full debug details of a given MiGo type, use the -D argument of Gong. It shows reachable states of the MiGo type, and also gives details on the liveness errors (if any).

Gong -D inferred.migo

Acknowledgements

We thank Juliana Franco and Takuma Ishikawa for their comments and testing.

• Julien Lange, Nicholas Ng, Bernardo Toninho, Nobuko Yoshida: Fencing off Go: Liveness and Safety for Channel-based Programming. POPL 2017 : 748 - 761.