dingo hunter

野狗

靜態分析儀，用於在Go中尋找僵局

這是一個靜態分析儀，用於建模並發並在GO代碼中找到死鎖。該工具的主要目的是從GO源代碼中推斷出其並發模型以兩種格式中的任何一種：

• 通信有限狀態機（CFSM）
• Migo類型

然後將推斷的模型傳遞給單獨的工具進行正式分析。在兩種方法中，我們都將文獻中已知的系統應用於會話類型，以尋找潛在的溝通不匹配以搶占潛在的僵局。

安裝

可以通過go get安裝dingo-hunter ，需要GO版本go1.7.1 。

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

用法

基於兩項研究工作，有兩種方法（CFSM和MIGO類型）。

CFSMS方法

該方法生成CFSM作為程序中產卵的Goroutines的模型，然後將CFSMS傳遞到合成工具中以構建全局編排並檢查有效性（請參閱論文）。

首先通過檢查子模塊來安裝合成工具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上運行CFSM生成：

 $ 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（即安全）。

限制

• 我們的工具目前僅支持同步（無封閉頻道）通信
• 在任何通信操作都不取決於這些通信之後，goroutines產生了。我們的模型假設Goroutines是獨立產卵的。

Migo類型方法

這種方法生成了Migo類型，這是本工作中引入的行為類型，以通過在通道使用情況下稱為圍欄的限制來檢查安全性和行為（請參閱論文）。

Migo類型的檢查器可在暱稱/鑼上找到，請按照說明來構建該工具：

 $ 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

限制

• 頻道目前不支持作為返回值
• 通道RECV，OK測試無法在Migo中表示（需要檢查值，但按類型抽象）

研究出版物

• 全球會話圖，Nicholas Ng和Nobuko Yoshida，INT'L編譯器建設會議（CC 2016），ACM的靜態僵局GO GO GO GO GO GO GO GO GO GO GO。
• 擊劍GO：基於渠道的編程的效果和安全性，Julien Lange，Nicholas Ng，Bernardo Toninho和Nobuko Yoshida，ACM Sigplan Sigplan Angrimium of編程語言原理（POPL 2017），ACM，ACM

筆記

這是一個研究原型，可能對所有GO源代碼不起作用。請提出一個看起來像錯誤的問題的問題。

執照

Dingo-Hunter已獲得Apache許可證的許可