Введение 3
Постановка задачи 6
1. Обзорный раздел по предметной области 7
1.1. Графы исполнения 7
1.2. Модели памяти 9
1.3. Алгоритм TruSt 10
1.4. Границы применимости TruSt 14
1.5. Язык Coq 15
1.6. Библиотека Hahn 16
2. Теоремы о Корректности и Терминируемости 18
2.1. TruSt в терминах отношений 18
2.2. Теорема о Корректности 19
2.3. Теорема о Терминируемости 19
3. Теоремы о Полноте и Оптимальности 23
3.1. Алгоритм Prev и его базовые свойства 23
3.2. Теорема о Полноте 27
3.3. Теорема об Оптимальности 28
Заключение 30
Список литературы 31
Проверка моделей без сохранения состояния (stateless model checking, SMC) [1,2] — это эффективный метод верификации конечных параллельных программ. Он был представлен как альтернатива проверке модели с явным сохранением состояния, которая позволяет избежать чрезмерного потребления памяти и, следовательно, имеет потенциал для масштабирования до более крупных программ. SMC работает систематически исследуя все сценарии исполнения программы данной параллельной программы, не сохраняя набор уже посещенных состояний программы.
Хотя SMC позволяет проверять программу с полиномиальными затратами по памяти, у него есть очевидный недостаток, заключающийся в том, что количество проверяемых исполнений обычно экспоненциально зависит от размера программы. Таким образом, SMC почти всегда используется вместе с продвинутыми алгоритмами динамической редукции частичного порядка (DPOR) [3,4, 5], сокращающими количество выполнений, которые необходимо изучить, чтобы охватить все поведения программы. DPOR разделяет трассы исполнения программы на классы эквивалентности по некоторому отношению, такому как эквивалентность Мацуркевича [6], с тем свойством, что все эквивалентные трассы показывают один и тот же наблюдаемый результат. Тогда для верификации программы достаточно исследовать по одной трассе из каждого класса эквивалентности.
Однако достижение оптимального алгоритма (в ходе работы которого, исследуется только одна трасса исполнения из каждого класса эквивалентности) — непростая задача. Алгоритмы DPOR (например, [7, 9, 10, 4, 5, 11]) обычно начинают с изучения одной трассы программы, и всякий раз, когда они обнаруживают пару обращений к памяти, находящихся в состоянии гонки, они исследуют дополнительные трассы, которые содержат такие обращения в обратном порядке, а также сохраняют некоторое состояние, чтобы избежать повторного исследования эквивалентных трасс исполнения. Однако существующие алгоритмы либо неоптимальные, что означает, что они могут исследовать экспоненциальное число трасс даже для программ с O(n) классами эквивалентности (где n — размер программы), либо достигают оптимальности, сохраняя какие-то исполнения программы и, следовательно, жертвуют тем, для чего SMC был придуман: полиномиальным потреблением памяти. На самом деле, большинство современных решений DPOR для проблемы верификации выбирают второе решение, т. е. они могут потреблять экспоненциальный объем памяти.
Наконец, командой института Макса Планка (Кайзерслаутерн, Германия) был представлен алгоритм TruSt (Truly Stateless Model-checker), который позволяет избежать данного компромисса. Он производит оптимальный DPOR и в тоже время работает с линейными затратами по памяти. Еще одно преимущество TruSt заключается в том, что он параметричен в выборе модели памяти, поддерживая не только модель последовательной согласованности (SC) [12], но и широкий спектр слабых моделей памяти, таких как модель TSO [13], PSO [14] uRC11 [15].
Однако реализация самого алгоритма нетривиальная. Ошибка в такой реализации приведет к тому, что алгоритм либо будет вводить пользователя в заблуждение, либо находить не все ошибки. Поэтому очень важно верифицировать такие алгоритмы.
Обычно доказательства корректности в области верификации многопоточных программ очень громоздкие и нетривиальные. Они требуют рассмотрения большого количества случаев, некоторые из которых доказываются механически. В этом деле человеку сложно учесть все детали и не допустить ошибок. В тоже время, как было описано ранее, выдвигаются повышенные требования к надежности. Чтобы преодолеть данную проблему, можно использовать системы автоматической проверки доказательств, например Coq [16]. Такие инструменты позволяют записывать формулировки различных теорем в качестве кода на соответствующем языке программирования, а затем в рамках того же языка строить доказательства. После система проверяет предъявленные доказательства на наличие ошибок. Подобный процесс взаимодействия с подобными системами называется механизацией доказательств. Механизация как раз и гарантирует корректность представленного кода. Системы по типу Coq очень хорошо показали себя в значительном количестве больших проектов. В частности, они были использованы для написания верифицированного компилятора языка C [27], ядра ОС [28], файловой системы [30], а так же для проверки доказательств теорем “Фейхта-Томпсона” [31] и “О четырех красках” [29].
Целью данной работы было получение механизированного доказательства корректности работы алгоритма TruSt используя аистему Coq.
В рамках данной дипломной работы были достигнуты следующие результаты.
• Было доказано, что алгоритм TruSt корректен, то есть он в ходе работы посещает только те графы исполнения, которые соответствуют заранее выбранной модели памяти.
• Была доказана терминируемость алгоритма TruSt на конечных программах, то есть он завершается если на вход дана программа с ограниченными графами исполнения
• Была доказана полнота алгоритма TruSt в случае конечных программ, то есть он посещает все графы исполнения конечных программ, соответствующие заранее выбранной модели памяти
• Была доказана оптимальность алгоритма TruSt в случае конечных программ, то есть он не посещает они и те же граф исполнения более одного раза
Все теоремы были механизированы в системе Coq.
