Skip to content
Static analyser for finding Deadlocks in Go
Branch: master
Clone or download
Latest commit 9756e4b Mar 14, 2019
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
cfsmextract Add test for self loop handling (#20). May 18, 2018
cmd
examples Fixes handling of empty select-default Oct 31, 2016
fairness Add simple fairness checker Jun 29, 2016
logwriter Add logging wrapper: logwriter Jun 29, 2016
migoextract Enable Go Modules and update library API. Jan 10, 2019
ssabuilder GetMainPkg --> MainPkg Nov 14, 2016
static Add support for CFSM demo in webservice Jan 6, 2017
talks Add Twitter handle Aug 20, 2016
templates Add support for CFSM demo in webservice Jan 6, 2017
third_party Update synthesis tool Feb 18, 2016
webservice Enable Go Modules and update library API. Jan 10, 2019
.gitignore .gitignore Jun 29, 2016
.gitmodules Update submodule to use public URL Feb 18, 2016
.travis.yml Update travis Go version. Jan 10, 2019
LICENSE Update LICENSE Jun 29, 2016
README.md Update README (close #23) Mar 13, 2019
doc.go Migrate to cobra Jun 29, 2016
go.mod Enable Go Modules and update library API. Jan 10, 2019
go.sum Enable Go Modules and update library API. Jan 10, 2019
main.go Fix build error and bump go version Oct 7, 2016

README.md

dingo-hunter Build Status

Static analyser for finding Deadlocks in Go

This is a static analyser to model concurrency and find deadlocks in Go code. The main purpose of this tool is to infer from Go source code its concurrency model in either of the two formats:

  • Communicating Finite State Machines (CFSMs)
  • MiGo types

The inferred models are then passed to separate tools for formal analysis. In both approaches, we apply a system known in the literature as Session Types to look for potential communication mismatches to preempt potential deadlocks.

Install

dingo-hunter can be installed by go get, go version go1.7.1 is required.

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

Usage

There are two approaches (CFSMs and MiGo types) based on two research work.

CFSMs approach

This approach generates CFSMs as models for goroutines spawned in the program, the CFSMs are then passed to a synthesis tool to construct a global choreography and check for validity (See paper).

First install the synthesis tool gmc-synthesis by checking out the submodule:

$ cd $GOPATH/src/github.com/nickng/dingo-hunter; git submodule init; git submodule update
$ cd third_party/gmc-synthesis

Follow README to install and build gmc-synthesis, i.e.

$ cabal install MissingH split Graphalyze
$ ./getpetrify # and install to /usr/local/ or in $PATH
$ ghc -threaded GMC.hs --make && ghc --make BuildGlobal

To run CFSMs generation on example/local-deadlock/main.go:

$ dingo-hunter cfsms --prefix deadlock example/local-deadlock/main.go

Output should say 2 channels, then run synthesis tool on extracted CFSMs

$ cd third_party/gmc-synthesis
$ ./runsmc inputs/deadlock_cfsms 2 # where 2 is the number of channels

The SMC check line indicates if the global graph satisfies SMC (i.e. safe) or not.

Limitations

  • Our tool currently support synchronous (unbuffered channel) communication only
  • Goroutines spawned after any communication operations must not depend on those communication. Our model assumes goroutines are spawned independenly.

MiGo types approach

This approach generates MiGo types, a behavioural type introduced in this work, to check for safety and liveness by a restriction called fencing on channel usage (See paper).

The checker for MiGo types is available at nickng/gong, follow the instructions to build the tool:

$ git clone ssh://github.com/nickng/gong.git
$ cd gong; ghc Gong.hs

To run MiGo types generation on example/local-deadlock/main.go:

$ dingo-hunter migo example/local-deadlock/main.go --no-logging --output deadlock.migo
$ /path/to/Gong -A deadlock.migo

Limitations

  • Channels as return values are not supported right now
  • Channel recv,ok test not possible to represent in MiGo (requires inspecting value but abstracted by types)

Research publications

Notes

This is a research prototype, and may not work for all Go source code. Please file an issue for problems that look like a bug.

License

dingo-hunter is licensed under the Apache License

You can’t perform that action at this time.