dingo hunter

Dingo-caçador

Analisador estático para encontrar impulsos

Este é um analisador estático para modelar a simultaneidade e encontrar impulsos no código GO. O principal objetivo desta ferramenta é inferir do código -fonte Go seu modelo de simultaneidade em qualquer um dos dois formatos:

• Comunicação de máquinas de estado finitas (CFSMS)
• Tipos MIGO

Os modelos inferidos são passados ​​para separar ferramentas para análise formal. Em ambas as abordagens, aplicamos um sistema conhecido na literatura como tipos de sessão para procurar possíveis incompatibilidades de comunicação para antecipar impulsos em potencial.

Instalar

dingo-hunter pode ser instalado pelo go get , GO Versão go1.7.1 é necessário.

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

Uso

Existem duas abordagens (CFSMs e tipos MIGO) com base em dois trabalhos de pesquisa.

Abordagem de CFSMS

Essa abordagem gera CFSMs como modelos para Goroutines gerados no programa, os CFSMs são passados ​​para uma ferramenta de síntese para construir uma coreografia global e verificar a validade (consulte o papel).

Primeiro instale a ferramenta de síntese gmc-synthesis verificando o submódulo:

 $ cd $GOPATH/src/github.com/nickng/dingo-hunter; git submodule init; git submodule update
$ cd third_party/gmc-synthesis

Siga README para instalar e construir gmc-synthesis , ou seja,

 $ cabal install MissingH split Graphalyze
$ ./getpetrify # and install to /usr/local/ or in $PATH
$ ghc -threaded GMC.hs --make && ghc --make BuildGlobal

Para executar o CFSMS Generation no example/local-deadlock/main.go :

 $ dingo-hunter cfsms --prefix deadlock example/local-deadlock/main.go

A saída deve dizer 2 canais e, em seguida, executar a ferramenta de síntese em CFSMs extraídos

 $ cd third_party/gmc-synthesis
$ ./runsmc inputs/deadlock_cfsms 2 # where 2 is the number of channels

A linha SMC check indica se o gráfico global satisfaz SMC (ou seja, seguro) ou não.

Limitações

• Atualmente, nossa ferramenta suporta apenas a comunicação síncrona (canal não sofrido)
• Goroutines gerados após quaisquer operações de comunicação não devem depender dessas comunicações. Nosso modelo assume que as goroutinas são geradas independentemente.

Abordagem dos tipos MIGO

Essa abordagem gera tipos MIGO, um tipo de comportamento introduzido neste trabalho, para verificar a segurança e a vivacidade por uma restrição chamada esgrima no uso do canal (consulte o papel).

O verificador para os tipos MIGO está disponível no apelo/gongo, siga as instruções para construir a ferramenta:

 $ git clone ssh://github.com/nickng/gong.git
$ cd gong; ghc Gong.hs

Para executar os tipos MIGO geração no example/local-deadlock/main.go :

 $ dingo-hunter migo example/local-deadlock/main.go --no-logging --output deadlock.migo
$ /path/to/Gong -A deadlock.migo

Limitações

• Canais como valores de retorno não são suportados agora
• Channel RECV, OK Teste Não é possível representar no MIGO (requer inspeção de valor, mas abstraído por tipos)

Publicações de pesquisa

• Detecção de deadlock estática para a síntese de gráficos de sessão global, Nicholas Ng e Nobuko Yoshida, conferência Int'l sobre construção de compiladores (CC 2016), ACM
• Cercando-se: LIGNIDADE E SEGURANÇA PARA A PROGRAMAÇÃO BASE DO CANAL, JULIEN LANGE, NICHOLAS NG, BERNARDO TONINHO e NOBUKO YOSHIDA, ACM SIGPLAN SIMPOSIUM SOBRE PRINCÍPIOS DE LÍNGUAS DE PROGRAMAÇÃO (POPL 2017), ACM

Notas

Este é um protótipo de pesquisa e pode não funcionar para todo o código -fonte Go. Por favor, arquive um problema para problemas que parecem um bug.

Licença

Dingo-Hunter é licenciado sob a licença Apache