Сборники трудов ИСП РАН


Конфигурируемый метод поиска состояний гонок в операционных системах с использованием предикатных абстракций

П.С. Андрианов (ИСП РАН, Москва, Россия)
В.С. Мутилин (ИСП РАН, Москва, Россия)
А.В. Хорошилов (ИСП РАН, Москва, Россия, МГУ, Москва, Россия, МФТИ, Долгопрудный, Россия, ВШЭ, Москва, Россия)

Аннотация

В статье представлен конфигурируемый метод для поиска состояний гонок. Метод позволяет настраивать требуемую точность анализа, выбирая баланс между затрачиваемыми ресурсами и количеством ложных предупреждений подключением двух расширений: уточнением путей на основе предикатных абстракций и анализом потоков. Метод основан на алгоритме Lockset и использует упрощенную модель памяти для уменьшения количества ложных предупреждений. Предлагаемый подход был реализован в инструменте CPALockator, который был апробирован на модулях ядра операционной системы Linux, что позволило обнаружить несколько состояний гонок, которые были признаны и исправлены разработчиками.

Ключевые слова

статический анализ, состояние гонки, ядро операционной системы

Издание

Труды Института системного программирования РАН, том 28, вып. 6, 2016, стр. 65-86.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2016-28(6)-5

Полный текст статьи в формате pdf Вернуться к содержанию тома