Метод легковесного статического анализа для поиска состояний гонок

В этой статье представлен подход легковесного статического анализа для поиска состояний гонок, названный CPALockator. Он учитывает такую специфику ядер операционных систем, как сложный параллелизм и особые примитивы синхронизации. Метод основан на алгоритме Lockset, но использует две эвристики, которые призваны уменьшить количество ложных предупреждений: модель памяти и модель параллелизма. В качестве примитивов синхронизации рассматриваются блокировки. Основным предметом нашего исследования являются ядра операционных систем, но предложенный подход может быть применен также и для других программ. Метод основан на идее адаптивного статического анализа (Configurable Program Analysis, CPA) и реализован в инструменте CPAchecker. Реализация метода состоит из двух стадий: сначала определяется множество разделяемых переменных для каждой точки программы, затем производится анализ примитивов синхронизации. На второй стадии собирается информация о всех возможных доступах к разделяемым переменным и захваченных примитивах синхронизации. После этого создается отчет, содержащий предупреждения для тех переменных, для которых было найдено хотя бы два доступа, образующие потенциальное состояние гонки. Для каждого доступа приводится один из возможных путей выполнения программы, который ведет к нему. Инструмент был апробирован на ядре операционной системы реального времени объемом приблизительно 200 000 строк кода. Он позволил найти 20 новых состояний гонки, признанных разработчиками. Кроме того, был произведен пилотный запуск инструмента на драйверах операционной системы Linux с помощью инфраструктуры инструмента LDV, который использовался для подготовки заданий для инструмента CPALockator. Дальнейшим направлением исследований является разработка более точной модели потоков, интеграция с более точными тяжеловесными техниками анализа.