Введение
1 Анализ методов и средств верификации протоколов когерентности памяти и постановка задачи 12
1.1 Проблема когерентности и протоколы когерентности 12
1.2 Проблема верификации протоколов когерентности 16
1.3 Формальные методы
1.3.1 Группы формальных методов 17
1.3.2 Метод анализа достижимости состояний и метод проверки моделей 19
1.3.3 Методы, основанные на доказательстве теорем 21
1.3.4 Сравнение методов проверки моделей и доказательства теорем и постановка задачи верификации параметризованных моделей 23
1.3.5 Методы абстракции 25
1.3.6 Методы, основанные на поиске сетевых инвариантов 30
1.3.7 Полные методы редукции 32
1.3.8 Методы композиционной проверки моделей 33
1.3.9 Методы, основанные на поиске инвариантов 36
1.4 Постановка задачи 40
Выводы по главе 1 42
2 Разработка абстрактных моделей протоколов когерентности 44
2.1 Выбор языка описания и спецификации моделей 44
2.1.1 Разработка модели протоколов когерентности в виде множества взаимодействующих конечных автоматов 44
2.1.2 Выбор языка и инструментального средства для описания моделей протоколов когерентности 46
2.2 Выбор математической модели для представления протоколов когерентности 49
2.2.1 Модель протоколов когерентности 49
2.2.2 Система переходов 50
2.2.3 Граф процесса 50
2.2.4 Канальная система
2.3 Разработка моделей протоколов когерентности на языке Promela и определение ограничений для них 58
2.4 Синтез совокупности преобразований, приводящих к получению абстрактной модели
2.4.1 Абстрактная модель протоколов когерентности 62
2.4.2 Абстрактные преобразования элементов множеств 66
2.4.3 Абстрактные преобразования элементов множеств 67
2.5 Математическое доказательство корректности процедуры абстракции 69
Выводы по главе 2 88
3 Разработка метода верификации протоколов когерентности памяти 90
3.1 Разработка Promela-моделей протоколов когерентности 90
3.1.1 Соответствие элементов Promela-моделей математическим абстракциям 90
3.1.2 Преобразования Promela-моделей
3.2 Процедура уточнения абстрактных моделей 97
3.3 Метод верификации протоколов когерентности памяти 100
3.4 Методика верификации протоколов когерентности памяти 100
Выводы по главе 3 102
4 Реализация и экспериментальные исследования системы верификации протоколов когерентности памяти 104
4.1 Составление формальных моделей протоколов когерентности на примере протокола системы на кристалле Эльбрус-4C 104
4.1.1 Анализ системы на кристалле Эльбрус-4С 104
4.1.2 Протокол когерентности системы на кристалле Эльбрус-4С 107
4.1.3 Разработка формальной модели протокола когерентности Эльбрус-4С 109
4.1.4 Уточнение абстрактной модели протокола Эльбрус-4С 112
4.2 Реализация инструмента построения внутреннего представления Promela моделей 116
4.2.1 Выбор внутреннего представления Promela-моделей 116
4.2.2 Разработка грамматики языка Promela с помощью средств Boost.Spirit 119
4.2.3 Разработка структур данных для дерева абстрактного синтаксиса 120
4.2.4 Обход дерева абстрактного синтаксиса и разработка алгоритмов, осуществляющих абстрактные преобразования 127
4.3 Сбор и обработка информации по результатам испытаний 138
4.3.1 Анализ требуемых ресурсов 138
4.3.2 Найденные ошибки и верификация протокола с ошибками 142
Выводы по главе 4 143
Выводы по диссертации 145
Список литературы
