Оглавление
Введение.
Актуальность темы.
Цель работы, задачи исследования
Научная новизна.
Практическая ценность.
Положения, выносимые на защиту.
Публикации и апробация результатов.
Краткое содержание работы
Глава 1. Обзор существующих подходов к анализу гонок
1.1. Обзор основных типов современных параллельных вычислительных систем.
Классификация параллельных архитектур
Современные направления развития параллельных вычислительных систем
Параллельные системы.
Взаимодействие потоков через разделяемую память
1.2. Состояние гонки
Методы синхронизации.
Синхронизация с блокировками.
Неблокирующаяся синхронизация
Транзакционная память
1.3. Обзор методов проверки правильности выполнения программ
Экспертиза.
Динамический анализ
Статический анализ.
Формальные методы
1.4 Классификация моделей.
Исполнимые модели
Ограничительные модели
Аксиоматические модели
Дополнительные виды моделей.
1.5. Классификация формальных методов
Методы проверки моделей.
Методы дедуктивного анализа.
Глава 2. Математическая модель.
2.1. Математическая модель.
2.2. Сепарационная логика
2.4. Синтаксис языка программирования
2.5. Операционная семантика
2.6 Утверждения. Формулы и аксиомы утверждений.
Глава 3. Метод верификации.
3.1 Обзор метода верификации Ле1уОиагап1ее
Комбинирование ИЛЗ и С8Ь
Метод ГЮ8ер и БАвЬ
Метод ЫЮ.
3.2. Переходы
3.4. Аксиомы и правила вывода
3.5. Доказательство непротиворечивости вывода
Глава 4. Спецификация формулы корректности.
4.1. Использование ЬТЬ логик для задания формулы корректности
4.2. Общая схема проведения анализа
4.3. Оценка сложности анализа на наличие гонок в параллельных программах
Глава 5. Примеры анализа многопоточных алгоритмов
5.1 Неблокирующаяся реализация алгоритма стека.
5.2. Неблокирующаяся реализация алгоритма очереди
5.3 Алгоритм булочной
Глава 6. Автоматизация.
8таГоог1Ш
Обзор среды каЬеНеНОЬ.
Описание комплекса программ
Заключение
Литература
- Київ+380960830922