Математическое моделирование алгоритмов, работающих на разделяемой памяти

• Автор: Кудрин, Максим Юрьевич
• Шифр специальности: 05.13.18
• Научная степень: Кандидатская
• Год защиты: 2009
• Место защиты: Москва
• Количество страниц: 112 с. : ил.

Оглавление
Оглавление
Введение

Актуальность темы.

Цель работы, задачи исследования .

Научная новизна.

Практическая ценность.

Краткое содержание работы.

Обзор существующих систем.

Динамический анализ

Общие принципы

Инструменты динамического анализа.
Средства статического анализа
Основные принципы.
Вычисления при помощи набора состояний
Анализ части кода.
Использование псевдонимов.
Точность и время работы.
Алгоритмы
Анализаторы
Синхронизация в многопоточных алгоритмах.
Архитектуры параллельных систем
Моделирование и методика анализа.
Алгоритмы анализа
Постановка задачи для двух потоков.
Представление работы потоков.
Построение графа совместного исполнения потоков
Определение классов эквивалентности
Построение представителей классов эквивалентности
Оценка числа классов эквивалентности.
Построение редуцированного графа и анализ
результатов
Анализ трех и большего числа потоков.
Ветвления в алгоритмах.
Допустимость перестановки операций одного потока
Примеры исследования многопоточных алгоритмов
Задача об изменении значения ячейки в двух потоках
Граф совместного исполнения потоков
Классы эквивалентности.
Редуцированный граф
Вычисление результата работы потоков.
Задача о транзакционном изменении двух ячеек памяти .
Представление работы потоков.
Граф совместного исполнения потоков
Классы эквивалентности.
Редуцированный граф
Вычисление результата работы потоков.
Алгоритм спинблокировки.
Ыеблокнрующаяся реализация алгоритма очереди.
Алгоритм Петерсона для случая двух потоков.
Заключение.
Список использованных источников


Проверка на основе моделей представляет собой метод верификации правильности работы конечного автомата, в котором применяется параллельная обработка. Этот метод позволяет формально обосновать отсутствие дефектов в тестируемой части кода на основе заданных разработчиком правил преобразования данных. В большинстве случаев невероятно сложно автоматически вывести модель из программного кода, а создание моделей вручную является ничуть не более простой операцией. Открытой проблемой является построение метода, которой позволит обнаружить все состояния гонок, приводящих к некорректной работе программы (дальше - неразрешенное состояние гонки), без ложных срабатываний. Наибольший интерес представляет автоматизированный анализ деблокирующихся реализаций различных алгоритмов, приобретающих все большую популярность. Такие реализации могут быть более безопасными и эффективными при большом количестве конкурирующих потоков исполнения, чем их классические аналоги, использующие синхронизационные примитивы. В работе предложен метод, позволяющий обнаружить неразрешенные состояния гонки и конкретные ситуации их возникновения в многопоточных алгоритмах, удовлетворяющих ряду ограничений. Метод не претендует на анализ произвольного алгоритма любой сложности - указанные неблокирующиеся реализации алгоритмов содержат относительно небольшое число строк кода, используемых ячеек памяти и ветвлений. Моделирование многопоточных алгоритмов, работающих на разделяемой памяти. Разработка критериев наличия состояний конкурентного доступа к памяти, приводящих к некорректной работе алгоритма. Разработка методики автоматизированного тестирования, определяющей наличие состояний конкурентного доступа к памяти, приводящих к некорректной работе многопоточной программы. Оценка сложности методики автоматизированного тестирования в различных случаях. Научная новизна работы заключается в предложенной методике формализации и моделирования процесса исполнения многопоточных алгоритмов. Разработанная методика автоматизированного тестирования для определенных условий может существенно уменьшить сложность анализа многопоточных алгоритмов. Результаты исследования могут быть использованы на практике для определения наличия состояний гонки, и применимы, в том числе, к анализу нсблокирующихся реализаций различных алгоритмов. В первой главе работы рассматриваются существующие методы поиска состояний гонки в многопоточных программах. Кроме того, приводятся сведения об алгоритмах, свободных от блокировок, как наиболее перспективной области приложения предложенной в работе методики. Вторая глава посвящена моделированию и методике анализа процесса исполнения многопоточных алгоритмов на платформах архитектуры х. Приводятся особенности архитектуры х, которые учтены в математической модели. Предлагается способ оценки правильной работы алгоритма с помощью внешней по отношению к анализируемому алгоритму функции корректности, которая выбирается исходя из задачи, решаемой алгоритмом. Для того, чтобы уменьшить сложность анализа, предлагается разбить всевозможные варианты процесса исполнения многопоточного алгоритма на классы эквивалентности. В случае, если из некоторых соображений ясно, что функция корректности должна быть одинакова для всех представителей классов эквивалентности, достаточно вычислить ее для отдельно взятого представителя класса эквивалентности. В третьей главе рассматриваются разработанные алгоритмы анализа в случае двух потоков исполнения и определенных видов функций корректности. Для некоторых алгоритмов получены оценки сложности в различных случаях. Показано, что эти оценки могут быть существенно лучше, чем сложность переборного варианта анализа. В четвертой главе с помощью описанной в работе методики исследован ряд многопоточных алгоритмов, в том числе один свободный от блокировок. Результаты исследования согласуются с известными фактами о данных алгоритмах и результатами анализа данных алгоритмов с помощью иных методов. В заключении описываются основные результаты и выводы работы.