dingo hunter

dingo-chasseur

Analyseur statique pour trouver des impasses

Il s'agit d'un analyseur statique pour modéliser la concurrence et trouver des impasses dans le code GO. Le but principal de cet outil est de déduire du code source GO son modèle de concurrence dans l'un des deux formats:

• Communiquer des machines d'État finies (CFSM)
• Types migo

Les modèles déduits sont ensuite transmis pour séparer des outils pour l'analyse formelle. Dans les deux approches, nous appliquons un système connu dans la littérature sous le nom de types de session pour rechercher des décalages de communication potentiels pour préempter les blocages potentiels.

Installer

dingo-hunter peut être installé par go get , GO Version go1.7.1 est requis.

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

Usage

Il existe deux approches (CFSMS et types Migo) basées sur deux travaux de recherche.

Approche CFSMS

Cette approche génère des CFSM en tant que modèles de goroutines engendrés dans le programme, les CFSM sont ensuite transmises à un outil de synthèse pour construire une chorégraphie globale et vérifier la validité (voir papier).

Installez d'abord l'outil de synthèse gmc-synthesis en consultant le sous-module:

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

Suivez README pour installer et construire gmc-synthesis , c'est-à-dire

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

Pour exécuter la génération CFSMS sur example/local-deadlock/main.go :

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

La sortie doit dire 2 canaux, puis exécuter l'outil de synthèse sur les CFSM extraits

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

La ligne SMC check indique si le graphique global satisfait SMC (c.-à-d. Safe) ou non.

Limites

• Notre outil prend actuellement en charge la communication synchrone (canal non tamponné) uniquement
• Les Goroutines ont engendré après toute opération de communication ne doit pas dépendre de ces communications. Notre modèle suppose que les goroutines sont engendrées indépendamment.

Approche des types Migo

Cette approche génère des types de Migo, un type de comportement introduit dans ce travail, pour vérifier la sécurité et la vivacité par une restriction appelée clôture sur l'utilisation des canaux (voir papier).

Le vérificateur de Migo Types est disponible sur surnom / gong, suivez les instructions pour construire l'outil:

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

Pour exécuter la génération de types Migo sur example/local-deadlock/main.go :

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

Limites

• Les canaux en tant que valeurs de retour ne sont pas pris en charge pour le moment
• Canal recv, ok test pas possible à représenter dans Migo (nécessite d'inspecter la valeur mais abstrait par type)

Publications de recherche

• Détection statique de l'impasse pour la synthèse de graphes de session globale par la session globale, Nicholas Ng et Nobuko Yoshida, conférence Int'l sur la construction du compilateur (CC 2016), ACM
• Fencing Off Go: Lively and Safety for Channel Basé sur la programmation, Julien Lange, Nicholas Ng, Bernardo Toninho et Nobuko Yoshida, ACM Sigplan Symposium sur les principes des langages de programmation (POPL 2017), ACM

Notes

Il s'agit d'un prototype de recherche et peut ne pas fonctionner pour tous le code source GO. Veuillez déposer un problème pour des problèmes qui ressemblent à un bogue.

Licence

Dingo-Hunter est concédé sous licence Apache