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

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