Скачать Deadlock_Racer - Deadlock_Racer Source Code Скачать

Deadlock_Racer

Другие категории

v1.0.1

Скачать

Тупик

Deadlock является статическим анализатором обнаружения потенциальных тупиков в программах C, реализованных в качестве плагина платформы FRAMA-C.

Основной алгоритм основан на существующем инструменте Racerx. Так называемый анализ блокировки пересекает график потока управления и вычисляет набор блокировков, хранящихся в любой точке программы. Когда блокировка B получена с точным замком, который уже содержит блокировку A, зависимость a -> b добавляется в блокировку. Каждый цикл в этом графике затем сообщается как потенциальный тупик.

Плагин использует EVA (плагин анализа значений FRAMA-C) для вычисления информации о мае-точке для параметров операций блокировки. Поскольку Ева не может быть назначенным анализом параллельных программ, мы сначала определяем все потоки в программе, а затем запускаем их для каждого потока отдельно с контекстами точек программы, где был создан поток. Результатом является затем недооценка, которая не учитывает интерлирование потока.

Пример

Этот пример демонстрирует вывод для программы с простым тупиком. Более сложный пример можно найти здесь.

 void * thread1 ( void * v )
{
    pthread_mutex_lock ( & lock1 );
    pthread_mutex_lock ( & lock2 );
    ...
    pthread_mutex_unlock ( & lock2 );
    pthread_mutex_unlock ( & lock1 );
}

void * thread2 ( void * v )
{
    pthread_mutex_lock ( & lock2 );
    pthread_mutex_lock ( & lock1 );
    ...
    pthread_mutex_unlock ( & lock1 );
    pthread_mutex_unlock ( & lock2 );
}

Выход:

 [kernel] Parsing simple_deadlock.c (with preprocessing)
[Deadlock] Deadlock analysis started
[Deadlock] === Assumed threads: ===
[Deadlock] main
[Deadlock] thread1
[Deadlock] thread2
[Deadlock] === Lockgraph: ===
[Deadlock] lock1 -> lock2
[Deadlock] lock2 -> lock1
[Deadlock] ==== Results: ====
[Deadlock] Deadlock between threads thread1 and thread2:
  
  Trace of dependency (lock2 -> lock1):
  In thread thread2:
      Lock of lock2 (simple_deadlock.c:20)
      Lock of lock1 (simple_deadlock.c:21)
  
  Trace of dependency (lock1 -> lock2):
  In thread thread1:
      Lock of lock1 (simple_deadlock.c:10)
      Lock of lock2 (simple_deadlock.c:11)

Установка

Текущая версия совместима с Vanadium Frama-C, его подробное руководство по установке можно найти в руководстве пользователя и требует версии OCAML не менее 4.12. Помимо Frama-C, Deadlock требует, чтобы после установки Opam были установлены пакеты:

 ounit2
containers

После установки зависимостей и клонирования этого хранилища, тупик может быть установлен следующим образом:

 cd Deadlock
make setup
make
make install

Вы также можете запустить тупик в Docker, либо используя docker run -it tdacik/deadlock , либо запустив make docker , чтобы создать изображение самой последней версии.

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

Самый простой способ запуска плагина - это:

 frama-c -deadlock source_file1.c source_file2.c ...

Для более расширенного использования см. Список вариантов командной строки для настройки анализа и руководства по графическим интерфейсу для визуализации результатов в приложении GUI FRAMA-C.

Связанные документы

Дачик Т. Статическое обнаружение тупика в Frama-C в процессе Excel@Fit'20 . Брно Технологический университет, факультет информационных технологий. 2020

Дачик Т. Статический анализ в окружающей среде Frama-C был сосредоточен на диссертации бакалавриата Frama-C. Брно Технологический университет, факультет информационных технологий. 2020-07-10. Под руководством Войнара Томаша.