« Автоматизация процесса поиска потенциальных взаимных блокировок в моделях многопоточного программного обеспечения » « Автоматизация процесса поиска потенциальных взаимных блокировок в моделях многопоточного программного обеспечения » Аспирант кафедры «Информационные системы и технологии» Парфилов И.В. Научный руководитель: д.т.н., профессор Шумилов Ю.Ю. Аспирант кафедры «Информационные системы и технологии» Парфилов И.В. Научный руководитель: д.т.н., профессор Шумилов Ю.Ю.

ПРОБЛЕМА ВЗАИМНЫХ БЛОКИРОВОК Многопоточная программа Пример взаимной блокировки потоков Поток 1 Поток ПОСтрок кода ПотоковОпераций синхронизации JDK419000Нет данных 1458 MS Singularity MS Dryad

ЗАДАЧА ПОИСКА ВЗАИМНЫХ БЛОКИРОВОК Разработка эффективного алгоритма поиска взаимных блокировок Проектирование и разработка программного средства анализа моделей многопоточного ПО Разработка графического интерфейса программного средства анализа моделей Проведение исследования быстродействия предложенных подходов к поиску взаимных блокировок 3

ОСОБЕННОСТИ ВЕРИФИКАЦИИ МНОГОПОТОЧНОГО ПО 4

ПРОВЕРКА МОДЕЛЕЙ Многопоточная программа Модель многопоточной программы Проверка модели Отсутствие потенциальных ситуаций взаимных блокировок Последовательность выполнения потоков, приводящая к их взаимной блокировке 5

ПРИМИТИВЫ СИНХРОНИЗАЦИИ Примитив синхронизацииОперации над примитивом Исключающий семафор (мьютекс)LOCK, L UNLOCK, U Сигнальная переменная без памяти WAIT, W EMIT, E BROADCAST, B Сигнальная переменная с памятьюWAIT, A POST, P Пример модели многопоточной программы 6

ПРИМЕР МОДЕЛИРОВАНИЯ 7 void function1() { pthread_mutex_lock(&Mutex1); pthread_mutex_lock(&Mutex2); … pthread_mutex_lock(&Mutex2); pthread_mutex_unlock(&Mutex1); } void function2() { pthread_mutex_lock(&Mutex2); pthread_mutex_lock(&Mutex1); … pthread_mutex_lock(&Mutex1); pthread_mutex_unlock(&Mutex2); } int main(int argc, char *argv[]) { pthread_create(&Thread1,NULL, function1,NULL); pthread_create(&Thread2,NULL, function2,NULL); } Модель многопоточной программы, составленная по исходному коду

ДОСТАТОЧНОЕ УСЛОВИЕ ОТСУТСТВИЯ ВЗАИМНЫХ БЛОКИРОВОК Пусть имеется система субъектов S = {S 1,..., S n } с точками ветвления и точками зацикливания. Проделаем для субъектов данной системы линеаризацию по точкам зацикливания. Получившуюся систему обозначим S 0. Рассмотрим все различные системы субъектов, составленные по следующему принципу: на i-ом месте в системе стоит субъект из декомпозиции S i 0. Предположим, что для каждой системы S 00 из этого множества выполнены два условия: для любого исключающего семафора (например, j-го) не выполняются соотношения вида t(S k 00, L j ) L t(S m 00, L j )), система S 00 слабо локально упорядочена относительно сигнальных переменных. Тогда в основной системе S нет потенциальных ситуаций взаимной блокировки. 8

АЛГОРИТМ ПРОВЕРКИ ДОСТАТОЧНОГО УСЛОВИЯ Построение частного и общего ориентированного графа системы Система субъектов Выделение сильно связных компонент (ССК) в частном орграфе с помощью алгоритма Тарьяна Достаточное условие отсутствия взаимных блокировок выполнено Проверка полученных ССК на предмет ложного срабатывания Выделение связных компонент (СК) в общем орграфе с помощью поиска в глубину Выделение сильно связных компонент в полученных связных компонентах Остались ли ССК? Достаточное условие отсутствия взаимных блокировок не выполнено Да Нет 9

ПРОГРАММНОЕ СРЕДСТВО АНАЛИЗА МОДЕЛЕЙ 10

РЕЗУЛЬТАТ ПРОВЕРКИ ДОСТАТОЧНОГО УСЛОВИЯ 11

РЕЗУЛЬТАТ АНАЛИЗА МОДЕЛИ 12

ИССЛЕДОВАНИЕ БЫСТРОДЕЙСТВИЯ РАЗЛИЧНЫХ ПОДХОДОВ Тестовая модель Количество субъектов Количество разных субъектов Количество различных средств синхронизации Всего операций над средствами синхронизации Модель Модель Модель Модель Модель Модель Модель Модель Модель Модель Модель Модель

ИССЛЕДОВАНИЕ БЫСТРОДЕЙСТВИЯ РАЗЛИЧНЫХ ПОДХОДОВ Deadlock AnalyzerSPIN Режим Поиск первой взаимной блокировки Поиск всех взаимных блокировок Проверка достаточного условия отсутствия взаимных блокировок Поиск первой взаимной блокировки Поиск всех взаимных блокировок модели Кол-во дед- локов Время, с Кол-во дедлоков Время, с Возможны ли дедлоки Время, с Кол-во дедлоков Время, с Кол-во дедлоков Время, с Не завершен Не завершен Не завершен Не завершен 10Не завершен Не завершен Не завершен Не завершен 14

ЗАКЛЮЧЕНИЕЗАКЛЮЧЕНИЕ 1.Разработан алгоритм проверки выполнения достаточного условия отсутствия потенциальных взаимных блокировок. 2.Разработано программное средство анализа моделей многопоточного программного обеспечения, реализующее метод проверки выполнения достаточного условия отсутствия потенциальных взаимных блокировок. 3.Разработаны программные модули, реализующие методы, основанные на исчерпывающем переборе всех состояний модели. 4.Разработан графический интерфейс пользователя программного средства анализа моделей многопоточного программного обеспечения. 5.Проведено исследование быстродействия всех предложенных подходов к задаче поиска взаимных блокировок в моделях многопоточного программного обеспечения. Показано, что для моделей с большим количеством потоков предложенный метод поиска является единственным применимым на практике. 15