dingo hunter
1.0.0
これは、同時性をモデル化し、GOコードでデッドロックを見つける静的アナライザーです。このツールの主な目的は、GOソースコードから2つの形式のいずれかのいずれかの並行性モデルを推測することです。
推定されたモデルは、正式な分析のために別々のツールに渡されます。両方のアプローチで、セッションタイプとして文献で知られているシステムを適用して、潜在的なデッドロックを先取りするための潜在的なコミュニケーションの不一致を探します。
dingo-hunter go get 、Goバージョンgo1.7.1でインストールできます。
$ go get -u github.com/nickng/dingo-hunter
2つの研究作業に基づいて、2つのアプローチ（CFSMとMigoタイプ）があります。
このアプローチは、プログラムで生成されたゴルチンのモデルとしてCFSMを生成し、CFSMは合成ツールに渡され、グローバルな振り付けを構築し、有効性を確認します（論文を参照）。
サブモジュールをチェックアウトして、最初に合成ツールgmc-synthesisをインストールします。
$ cd $GOPATH/src/github.com/nickng/dingo-hunter; git submodule init; git submodule update
$ cd third_party/gmc-synthesis
READMEをフォローして、 gmc-synthesisをインストールして構築します
$ cabal install MissingH split Graphalyze
$ ./getpetrify # and install to /usr/local/ or in $PATH
$ ghc -threaded GMC.hs --make && ghc --make BuildGlobal
example/local-deadlock/main.goでCFSMSの生成を実行するには：
$ dingo-hunter cfsms --prefix deadlock example/local-deadlock/main.go
出力は2つのチャネルと言ってから、抽出されたCFSMで合成ツールを実行する必要があります
$ cd third_party/gmc-synthesis
$ ./runsmc inputs/deadlock_cfsms 2 # where 2 is the number of channels
SMC checkラインは、グローバルグラフがSMC（すなわち安全）を満たしているかどうかを示します。
このアプローチでは、この作業で導入された行動タイプであるMigoタイプが生成され、チャネルの使用に関するフェンシングと呼ばれる制限によって安全性と活性を確認します（論文を参照）。
MigoタイプのチェッカーはNickng/Gongで入手できます。指示に従ってツールを作成します。
$ git clone ssh://github.com/nickng/gong.git
$ cd gong; ghc Gong.hs
example/local-deadlock/main.goでMigoタイプの生成を実行するには：
$ dingo-hunter migo example/local-deadlock/main.go --no-logging --output deadlock.migo
$ /path/to/Gong -A deadlock.migo
これは研究プロトタイプであり、すべてのGOソースコードで機能しない場合があります。バグのように見える問題について問題を提出してください。
Dingo-Hunterは、Apacheライセンスの下でライセンスされています
