README
¶
dingo-hunter 
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 infer 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
- Static Deadlock Detection for Concurrent Go by Global Session Graph Synthesis, Nicholas Ng and Nobuko Yoshida, Int'l Conference on Compiler Construction (CC 2016), ACM
- Fencing off Go: Liveness and Safety for Channel-based Programming, Julien Lange, Nicholas Ng, Bernardo Toninho and Nobuko Yoshida, ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017), ACM
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
Documentation
¶
Overview ¶
Command dingo-hunter is a tool for analysing Go code to extract the communication patterns for deadlock analysis.
The deadlock analysis approach is based on multiparty session types and global graph synthesis POPL'15 (Lange, Tuosto, Yoshida) and CC'16 (Ng, Yoshida).
Source Files
Directories
¶
| Path | Synopsis |
|---|---|
|
sesstype
Package sesstype encapsulates representation of session types As opposed to role-based session types, this representation is channel-based.
|
Package sesstype encapsulates representation of session types As opposed to role-based session types, this representation is channel-based. |
|
examples
|
|
|
cond-recur
Command conditional-recur has a recursion with conditional on one goroutine and another receiving until a done message is received.
|
Command conditional-recur has a recursion with conditional on one goroutine and another receiving until a done message is received. |
|
forselect
Command nodet-for-select is a for-select pattern between two compatible recursive select.
|
Command nodet-for-select is a for-select pattern between two compatible recursive select. |
|
golang-blog-prime-sieve
Command golang-blog-prime-sieve is an example from Golang blog.
|
Command golang-blog-prime-sieve is an example from Golang blog. |
|
infinite-prime-sieve
Command infinite-primesieve is a modified primesieve example from Golang blog.
|
Command infinite-primesieve is a modified primesieve example from Golang blog. |
|
multiple-timeout
Command multiple-timeout is an example which uses multiple branches of time.After.
|
Command multiple-timeout is an example which uses multiple branches of time.After. |
|
parallel-buffered-recursive-fibonacci
Command parallel-recursive-fibonacci is a recursive fibonacci which spawns a new goroutine per fib call.
|
Command parallel-recursive-fibonacci is a recursive fibonacci which spawns a new goroutine per fib call. |
|
parallel-recursive-fibonacci
Command parallel-recursive-fibonacci is a recursive fibonacci which spawns a new goroutine per fib call.
|
Command parallel-recursive-fibonacci is a recursive fibonacci which spawns a new goroutine per fib call. |
|
parallel-twoprocess-fibonacci
Command parallel-twoprocess-fibonacci is an improved version of parallel fibonacci which limits to only spawning 2 goroutines.
|
Command parallel-twoprocess-fibonacci is an improved version of parallel fibonacci which limits to only spawning 2 goroutines. |
|
popl17/cond-recur
Command conditional-recur has a recursion with conditional on one goroutine and another receiving until a done message is received.
|
Command conditional-recur has a recursion with conditional on one goroutine and another receiving until a done message is received. |
|
popl17/fib
Command parallel-recursive-fibonacci is a recursive fibonacci which spawns a new goroutine per fib call.
|
Command parallel-recursive-fibonacci is a recursive fibonacci which spawns a new goroutine per fib call. |
|
popl17/fib-async
Command parallel-recursive-fibonacci is a recursive fibonacci which spawns a new goroutine per fib call.
|
Command parallel-recursive-fibonacci is a recursive fibonacci which spawns a new goroutine per fib call. |
|
popl17/forselect
Command nodet-for-select is a for-select pattern between two compatible recursive select.
|
Command nodet-for-select is a for-select pattern between two compatible recursive select. |
|
popl17/sieve
Command infinite-primesieve is a modified primesieve example from Golang blog.
|
Command infinite-primesieve is a modified primesieve example from Golang blog. |
|
squaring-cancellation
Command squaring-cancellation comes from Golang blog to demonstrate fan-in and explicit cancellation.
|
Command squaring-cancellation comes from Golang blog to demonstrate fan-in and explicit cancellation. |
|
squaring-fanin
Command squaring-fainin comes from Golang blog to demonstrate fan-in and explicit cancellation.
|
Command squaring-fainin comes from Golang blog to demonstrate fan-in and explicit cancellation. |
|
squaring-fanin-bad
Command squaring-fanin-bad comes from Golang blog to demonstrate fan-in and explicit cancellation.
|
Command squaring-fanin-bad comes from Golang blog to demonstrate fan-in and explicit cancellation. |
|
squaring-pipeline
Command squaring-pipeline comes from Golang blog to demonstrate fan-in and explicit cancellation.
|
Command squaring-pipeline comes from Golang blog to demonstrate fan-in and explicit cancellation. |
|
Package fairness runs a fairness analysis.
|
Package fairness runs a fairness analysis. |
|
Package logwriter wraps a io.Writer for dingo-hunter logging.
|
Package logwriter wraps a io.Writer for dingo-hunter logging. |
|
Package migoextract provides session type inference from Go code.
|
Package migoextract provides session type inference from Go code. |
|
Package ssabuilder provides a wrapper for building SSA IR from Go source code.
|
Package ssabuilder provides a wrapper for building SSA IR from Go source code. |
|
callgraph
Package callgraph represents function call graph.
|
Package callgraph represents function call graph. |