dingo hunter下载 - dingo hunter源代码下载

dingo hunter

其他类别

1.0.0

下载

野狗

静态分析仪，用于在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