Анализ корректности синхронизации компонентов ядра операционных систем

Большинство современных инструментов статической верификации плохо масштабируются на сложное программное обеспечение. Целью работы была разработка инструмента, который станет золотой серединой между точными и медленными инструментами статической верификации и быстрыми, но менее точными инструментами статического анализа. Основной идеей подхода является абстракция от точного взаимодействия потоков и анализ каждого потока отдельно от всех остальных, но в некотором окружении, которое моделирует влияние потоков друг на друга. Окружение содержит описание возможных действий над разделяемыми данными и примитивами синхронизации, а также условий их применения. Варьируя точность построения окружения, можно добиваться необходимого баланса между скоростью и точностью анализа в целом. Формальное описание предлагаемого подхода было сделано с использованием теории адаптивного статического анализа. Это позволило сформулировать условия и доказать корректность предлагаемого подхода в этих условиях. Для эффективного поиска состояний гонки используется специальная модель памяти, которая позволяет разделять области памяти на непересекающиеся регионы, соответствующие типам данных. Реализация предложенного подхода во фреймворке CPAchecker позволяет переиспользовать существующие техники анализа с минимальными изменениями. А реализация дополнительных техник анализа в рамках предложенной теории позволяет повысить точность анализа. Результаты проведенных экспериментов на двух наборах тестовых задач позволяют заключить о масштабируемости и практической применимости метода.