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