dingo hunter

Динго-Хантер

Статический анализатор для поиска тупиков в Go

Это статический анализатор для моделирования параллелизма и найти тупики в коде GO. Основная цель этого инструмента - сделать вывод из Go SourceD -кода его модели параллелизма в любом из двух форматов:

• Общение с конечными государственными машинами (CFSMS)
• Типы миго

Предполагаемые модели затем передаются в отдельные инструменты для формального анализа. В обоих подходах мы применяем систему, известную в литературе в качестве типов сеансов для поиска потенциальных несоответствий связи, для предотвращения потенциальных тупиков.

Установить

dingo-hunter может быть установлен с помощью go get , Go версия go1.7.1 требуется.

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

Использование

Существует два подхода (CFSM и типы MIGO) на основе двух исследовательских работ.

Подход CFSMS

Этот подход генерирует CFSMS как модели для Goroutines, порожденных в программе, CFSM затем передаются в инструмент синтеза для построения глобальной хореографии и проверки на обоснованность (см. Документ).

Сначала установите инструмент синтеза 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

Чтобы запустить генерацию CFSMS на example/local-deadlock/main.go :

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

Выход должен сказать 2 канала, а затем запустить инструмент синтеза на извлеченных CFSMS

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

Строка SMC check указывает, удовлетворяет ли глобальный график SMC (т.е. безопасен) или нет.

Ограничения

• Наш инструмент в настоящее время поддерживает только синхронную (не беспрепятственный канал).
• Goroutines породились после того, как любые операции по коммуникациям не должны зависеть от этих коммуникаций. Наша модель предполагает, что горутины появляются независимо.

Подход типов MIGO

Этот подход генерирует типы MIGO, поведенческий тип, введенный в этой работе, для проверки безопасности и жизнеобеспечения с помощью ограничения, называемого ограждением на использовании канала (см. Paper).

Проверка для типов MIGO доступна в Nickng/Gong, следуйте инструкциям по созданию инструмента:

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

Чтобы запустить генерацию типов типов MIGO example/local-deadlock/main.go :

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

Ограничения

• Каналы как возвращаемые значения не поддерживаются прямо сейчас
• Канал Recv, тест OK невозможно представлять в MIGO (требует осмотра значения, но абстрактно по типам)

Исследовательские публикации

• Статическое обнаружение тупика для одновременного Go By Global Session Graph Synthesis, Николас Нг и Нобуко Йошида, Int'l Conference по строительству компилятора (CC 2016), ACM
• Ограждение от Go: Lifence and Safety для программирования на основе каналов, Джульен Ланге, Николас Н.Г., Бернардо Тонинью и Нобуко Йошида, симпозиум ACM Sigplan по принципам языков программирования (Popl 2017), ACM

Примечания

Это исследовательский прототип, и может не работать для всех исходного кода GO. Пожалуйста, подайте проблему для проблем, которые выглядят как ошибка.

Лицензия

Dingo-Hunter имеет лицензию по лицензии Apache