Инструментальные средства Эффективные алгоритмы № 6 (36) 2011 ПРИКЛАДНАЯ ИНФОРМАТИКА Н. В. <...> Заборовский, аспирант Московского физико-технического института (государственного университета) А. Г. Тормасов, докт. физ.-мат. наук, профессор Московского физико-технического института (государственного университета) Статическое обнаружение гонок в коде, содержащем ветвления и циклы В настоящее время весьма актуальными являются задачи, связанные с реализацией многопоточных алгоритмов. <...> Данная работа посвящена анализу корректности неблокирующих алгоритмов в смысле состояний гонки. <...> Введение С остояние гонки — ситуация, когда состояние общей для нескольких потоков ячейки памяти зависит от распределения процессорного времени между потоками (фактически нельзя предугадать это состояние на уровне алгоритма — скорее всего, в реализации алгоритма ошибка). <...> Модель, построенная на основе предлагаемого подхода, позволяет отслеживать ситуации гонки для одной из разделяемых переменных и может быть расширена, в частности, до анализа корректности организованных средствами языка критических секций. <...> Обзор методов В работе [3] приводятся результаты формального аналитического доказательства корректности неблокирующего алгоритма, в том числе корректности в смысле отсутствия гонок. <...> В работе [2] была предложена идея построения модели взаимного исполнения ато38 Инструментальные средства Эффективные алгоритмы марных инструкций двумя потоками на разделяемой памяти и принцип ее анализа с целью определения состояния гонки. <...> Общая процедура работы с исходным кодом для выявления состояний гонки выглядит следующим образом: 1. <...> Для каждого потока выделяются операции с интересующими нас разделяемыми переменными. <...> Строится граф на основании операций с разделяемыми переменными. <...> На графе выделяются определенные пути, представляющие интерес для анализа. <...> Выделенные пути анализируются, например, с помощью метода неопределенных <...>