dingo hunter
1.0.0
동시성을 모델링하고 GO 코드에서 교착 상태를 찾는 정적 분석기입니다. 이 도구의 주요 목적은 GO 소스 코드에서 동시성 모델을 두 가지 형식 중 하나로 추론하는 것입니다.
그런 다음 추론 된 모델을 전달하여 공식적인 분석을위한 별도의 도구로 전달됩니다. 두 가지 접근법 모두에서, 우리는 문헌에 알려진 시스템을 세션 유형 으로 적용하여 잠재적 인 교착 상태를 선점하기 위해 잠재적 커뮤니케이션 불일치를 찾습니다.
dingo-hunter go get , Go 버전 go1.7.1 에 의해 설치 될 수 있습니다.
$ go get -u github.com/nickng/dingo-hunter
두 가지 연구 작업을 기반으로 두 가지 접근 방식 (CFSMS 및 Migo 유형)이 있습니다.
이 접근법은 프로그램에서 스폰 된 고루 틴에 대한 모델로서 CFSM을 생성하고, 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 에서 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 (IE Safe)를 만족하는지 여부를 나타냅니다.
이 접근법은이 작업에 도입 된 행동 유형 인 Migo 유형을 생성하여 채널 사용에 대한 펜싱 이라는 제한으로 안전과 라이벌을 확인합니다 (논문 참조).
Migo 유형의 검사기는 Nickng/Gong에서 제공되며 지침을 따라 도구를 작성하십시오.
$ git clone ssh://github.com/nickng/gong.git
$ cd gong; ghc Gong.hs
example/local-deadlock/main.go 에서 Migo Type Generation을 실행하려면 :
$ dingo-hunter migo example/local-deadlock/main.go --no-logging --output deadlock.migo
$ /path/to/Gong -A deadlock.migo
이것은 연구 프로토 타입이며 모든 GO 소스 코드에 대해 작동하지 않을 수 있습니다. 버그처럼 보이는 문제에 대한 문제를 제기하십시오.
Dingo-Hunter는 Apache 라이센스에 따라 라이센스가 부여됩니다
