Static analyser for finding Deadlocks in Go
This is a static analyser to model concurrency and find deadlocks in Go code. We use a system known in the literature as Session Types to look for potential communication mismatches to preempt potential deadlocks.
$ go get -u github.com/nickng/dingo-hunter $ cd $GOPATH/nickng/dingo-hunter $ git submodule init; git submodule update $ cd third_party/gmc-synthesis
README to install and build
$ cabal install MissingH split Graphalyze $ ./getpetrify # and install to /usr/local/ or in $PATH $ ghc -threaded GMC.hs --make && ghc -make BuildGlobal
To run dingo-hunter on
$ dingo-hunter -p deadlock example/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
SMC check line indicates if the global graph satisfies SMC (i.e. safe) or not.
dingo-hunter is licensed under the Apache License