автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.18, диссертация на тему:Расчетная модель для нахождения состояния гонки в многопоточных алгоритмах

0050021 о**

На правах рукописи

Заборовский Никита Владимирович

РАСЧЕТНАЯ МОДЕЛЬ ДЛЯ НАХОЖДЕНИЯ СОСТОЯНИЙ ГОНОК В МНОГОПОТОЧНЫХ АЛГОРИТМАХ

Специальность 05.13.18 - математическое моделирование, численные методы и комплексы программ

АВТОРЕФЕРАТ

диссертации на соискание ученой степени кандидата физико-математических наук

2 4 НОЯ 2011

Москва-2011

005002184

Работа выполнена на кафедре информатики Московского физико-технического института (государственного университета)

Научный руководитель:

доктор физико-математических наук, профессор ТОРМАСОВ Александр Геннадьевич.

Официальные оппоненты:

доктор технических наук ДРОЗДОВ Александр Юльевич,

кандидат физико-математических наук СОКОЛОВ Евгений Владимирович

Ведущая организация:

Вычислительный центр им. А. А. Дородницына РАН

Защита состоится {5 декабря 2011 года в £ 0 часов на заседании диссертационного совета Д 212.156.05 при Московском физико-техническом институте (государственном университете) по адресу: 141700, Московская обл., г. Долгопрудный, Институтский пер., д. 9, ауд. 903 КПМ.

С диссертацией можно ознакомиться в библиотеке Московского физико-технического института (государственного университета).

Автореферат разослан ноября 2011 года.

Ученый секретарь диссертационного совета

Федько О.С.

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность темы

Многопоточная организация программ достаточно давно применяется программистами. При одноядерной архитектуре процессоров использование нескольких потоков обеспечивало упрощение процесса программирования, работу с блокирующими операциями и т.д. Чтобы эффективно использовать современные аппаратные платформы, нужны совершенно новые принципы и подходы. Под «эффективностью» понимается выигрыш от использования многоядерной платформы по сравнению с одноядерной. Иногда программы, написанные для одноядерной архитектуры, запускают на четырехядерной в надежде получить прирост производительности, а в результате оказывается, что производительность исполнения таких программ даже уменьшается.

Универсальных способов создавать эффективные программы не существует. Подход для каждой - строго индивидуален. Создание новых многопоточных программ даёт возможность подобрать для индивидуальной задачи по-настоящему подходящий и эффективный алгоритм. Как одно из решений можно упомянуть неблокирующие алгоритмы - альтернативу алгоритмам, использующим явные средства синхронизации.

Отсутствие универсальных подходов влечёт за собой также возможные ошибки программистов. Одной из наиболее сложных для обнаружения ошибок является состояние гонки. Состояния гонки (race condition, конкурентного доступа к памяти) - ситуация, когда состояние общей для нескольких потоков ячейки памяти зависит от распределения процессорного времени между потоками. Предугадать это состояние на уровне алгоритма невозможно. Понять аналитически, что возникло состояние гонки, очень сложно, т.к. для этого требуется анализ экспоненциально растущего количества ситуаций. Именно поэтому так важно контролировать программы ещё на стадии описания. Создание средств контроля корректности программ становится всё более необходимым с выпуском каждого нового процессора и написанием каждого нового сложного программного комплекса.

Различают два принципиально разных подхода к анализу многопоточных алгоритмов на предмет наличия состояний гонки: динамический и статический. Динамический подход представляет собой эмпирическую процедуру «прогона» программы при различных входных данных (data-race-test в Google, Intel Thread Checker). Принципиальный недостаток подхода в целом - невозможно проверить сложную систему, поскольку количество тестов экспоненциально зависит от числа входных параметров. Статический подход анализирует архитектуру программы и программный код без его запуска. К статическому анализу относится формальное доказательство корректности кода программы. Для современных программных продуктов сложность формального доказательства значительна, что делает его неприменимым в промышленных масштабах. Кроме того, есть вероятность ложного срабатывания. Один и тот же алгоритм может содержать состояние гонки и не содержать его в зависимости от значений входных параметров.

Цели работы, задачи исследования

Существует несколько подходов к статическому анализу кода неблокирующих алгоритмов в поисках состояния гонки. Однако, большая часть из них носит чисто теоретический характер, подходит только для модельных задач и дает неточные результаты (большой процент ложных срабатываний и не обнаружений гонки, когда она есть, false-negative). Необходим подход к анализу исходных кодов современных прикладных программ, учитывающий их сложность и специфику.

Для этого, во-первых, необходимо разработать математическую модель, представляющую ход исполнения потоков с точки зрения работы с общими разделяемыми переменными. Модель должна быть применима для анализа реальных современных программ и моделировать исполнение современной многопоточной программы.

Во-вторых, на основе этой модели должен быть разработан метод, позволяющий:

• определять состояние гонки, если оно есть, не давая ложных срабатываний в определенном классе задач;

• давать результат за время, приемлемое для использования при тестировании программных продуктов внутри компании-разработчика.

Кроме модели и метода должен быть создан комплекс программ, анализирующий многопоточные алгоритмы с целью выявления состояний гонки и обладающий следующими свойствами:

• возможность анализировать исходный код на языках высокого уровня и выдавать промежуточное представление исходного кода, аналогичное тому, которое получается на стадии компиляции программы;

• реализация разработанного метода и указание мест возникновения гонки и приводящих к ней условий.

Научная новизна

Научная новизна работы заключается в математическом моделировании поведения многопоточных алгоритмов, содержащих вервления и циклы, использующих разделяемую память. Математическая модель, предлагаемая в работе, учитывает начальные и промежуточные значения разделяемых переменных. Для модели разработана методика поиска состояний гонки в программном коде для определенного класса задач.

Хорошо известен ряд динамических и синтаксических анализаторов, обладающих следующими недостатками: тяжеловесность, зависимость от контекста, малая точность. Разработанный метод не зависит от контекста, определяет состояние гонки, если оно есть, и не даёт ложных срабатываний. Что касается тяжеловесности, то для статических анализаторов эта проблема стоит менее остро, чем для динамических. В работе в качестве примера приведён легковесный алгоритм анализа.

Практическая ценность

Созданные модель и метод ориентированы на практическую реализацию. В работе предложены методика анализа кода на присутствие состояния гонки, использующая некое промежуточное представления кода, и техническая реализация получения промежуточного представления из исходного кода. В качестве средства обработки исходного кода может быть использовано любое другое подходящее средство, позволяющее получить специфицированное промежуточное представление.

Положения, выносимые на защиту

1. Математическая модель исполнения многопоточных программ, учитывающая зависимость исполнения от начальных значений разделяемых переменных и описывающая, в том числе, такие конструкции программного кода как циклы, ветвления и атомарные операции.

2. Общий метод анализа многопоточных алгоритмов на предмет наличия гонок, в основе которого лежит анализ значений разделяемых переменных, и критерии корректности алгоритмов в понятиях разработанной модели.

3. Комплекс программ и результаты вычислительных экспериментов для выявления наличия гонок в некоторых многопоточных алгоритмах, в том числе неблокирующих.

Публикации и апробация результатов

По теме диссертации опубликовано 12 работ, в том числе три [1,2,3] - в изданиях, рекомендованных ВАК РФ.

Результаты работы докладывались и получили одобрение специалистов на научных семинарах и конференциях:

- XXXVI и XXVII международные молодежные научные конференции «Гагаринские чтения» (Москва, 2009,2010 г.),

- 5-ая международная конференция им. П.Л. Чебышева (Ногинск, 2011 г.),

- XVI Международная научная конференция студентов, аспирантов и молодых учёных «ЛОМОНОСОВ- 2009» (Москва, 2009 г.),

- 49-ая и 53-ая научные конференции МФТИ (Москва, 2007,2009 г).

Структура и объем работы

Диссертация состоит из введения, пяти глав, заключения и списка использованных источников. Работа изложена на 104 страницах, список использованных источников содержит 62 наименования.

СОДЕРЖАНИЕ РАБОТЫ

Во введении обосновывается актуальность диссертации, и формулируются ее цели, характеризуются научная новизна и практическая ценность работы.

Первая глава

В первой главе приводится краткий обзор существующих методов анализа исходного кода с точки зрения его корректности, а также реализующих их программных средств. Приводятся примеры статических анализаторов, указываются известные проблемы и возможные пути решений. Рассматриваются такие анализаторы как Viva64, Intel thread checker, data-race-test, KISS, CHESS и другие.

Вторая глава

Во второй главе описывается один из подходов к моделированию многопоточных исполнений алгоритмов, взятый за основу в данной работе.

Основы моделирования многопоточного исполнения

Уже известна идея построения модели взаимного исполнения атомарных инструкций двумя потоками на разделяемой памяти и принцип ее анализа с целью определения состояния гонки. Общая процедура работы с исходным кодом для выявления состояний гонки следующая:

1. Дня каждого потока выделяются операции с интересующими нас разделяемыми переменными.

2. Строится граф, определенный ниже, на основании операций с разделяемыми переменными.

3. На графе выделяются определенные пути.

4. Выделенные пути анализируются, например, с помощью метода неопределенных коэффициентов.

5. По состоянию в финальной вершине делается вывод о наличии гонок.

В основе модели лежит граф совместного исполнения потоков G.

Путям графа в соответствуют всевозможные варианты исполнения многопоточного алгоритма. Вершинам графа V соответствует множество состояний общей памяти после выполнения очередной инструкции, дугам А -атомарные операции над разделяемыми переменными. Каждому ребру поставлена в соответствие операция (Я — чтение, У/ — запись) и ячейка памяти, над которой производится операция.

Граф О имеет вид ромба, в котором начальная вершина находится вверху, а конечная - внизу, а все ребра имеет направление сверху вниз. Начальная вершина

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

- единичная атомарная операция. После совершения потоком очередной операции

G - (V, А),

V = и v', А= U (y'j»v

/+1 j

)и U (v'^J (1)

■•41 J J

) происходит переход системы из состояния в состояние ^ / . Конечная вершина - финальное состояние исполнения потоков.

Построение графа совместного исполнения п потоков

Покажем, как строится расчетный граф для двух потоков. Имеем начальную вершину, в которой состояние системы определяется значениями, которыми

проинициализированы переменные. Множество

ребер А будем обозначать как а;, где 1 — номер операции первого потока, а ] — второго. Тогда каждой вершине можно присвоить два индекса, означающие количество операций, выполненных каждым из потоков, чтобы оказаться в этой вершине. Из каждой вершины

^ 1, считая от начальной, будет исходить два

ребра: "у и до тех пор, пока в одном из потоков не закончатся операции — тогда из вершины будет исходить только одно ребро, соответствующее операции другого потока. Построенный таким образом граф, как уже было сказано, имеет вид ромба (рис. 1). Метод построения обобщается на случай п > 2 потоков: вершины и ребра будут иметь п индексов, а из каждой вершины будет исходить не менее п ребер. В общем случае граф совместного исполнения п потоков будет иметь вид п-мерного ромбовидного графа.

Для модели также определена функция корректности, отражающая субъективное понятие о корректном или некорректном исполнении программы. Одна и та же многопоточная программа может быть корректной с точки зрения одной функции корректности и некорректной - с другой. Отметим, что часто функцию корректности можно переформулировать в терминах частей графа в. К примеру, задача о нахождении неразрешенного состояния гонки может быть сведена к наличию двух различных путей на графе, приводящих к различным значениям одной из разделяемых переменных.

Сильное место подхода — небольшая сложность анализа. Количество вершин на каждом из ребер ромба линейно по количеству операций, и каждая вершина проходится при анализе только один раз. Таким образом, можно оценить, что сложность подхода для двух потоков - О(к п), где кип- количество атомарных операций каждого из потоков. Важно заметить, что рассматриваются только операции с разделяемыми переменными.

Далее с построенным графом поступаем следующим образом. Рассматриваем произвольный путь на графе из начальной вершины в конечную. Такой путь описывает взаимную последовательность исполнения атомарных

VI

V,'

Рис. 1. Граф совместного исполнения двух потоков на разделяемой памяти.

операций потоками. При проходе обращаем внимание на то, что есть вершины, из которых исходят рёбра с операциями над разными ячейками памяти или только операциями чтения одной и той же разделяемой переменной. В таком случае из вершины можно двигаться по любому из исходящих ребер - на состояние памяти в финальном состоянии это не повлияет. В остальных случаях результат алгоритма будет зависеть от порядка исполнения инструкций - от того, какой из путей из вершины будет выбран. При этом операции на рёбрах назовём не коммутирующими, а соответствующую ячейку графа пометим крестом (рис. 1).

На этом наблюдении основывается построение классов эквивалентности -наборов полных путей на графе G, для которых содержимое ячеек памяти в финальном состоянии одинаково. После нахождения всех классов путей, достаточно взять по одному представителю из каждого класса, чтобы охватить все возможные последовательности смены ячеек памяти.

Третья глава

В третьей главе излагаются сложности и узкие места при статическом анализе программного кода существующими методами. Рассматривается реальный практический код, часто имеющий сложную структуру, содержащий циклы и ветвления, а также атомарные операции.

Проблемы современных систем статического анализа

Для существующих в настоящее время средств настоящей проблемой является ошибочное определение состояния гонки (false-positive) и не нахождение гонки при ее наличии (false-negative). Такие проблемы неминуемо возникают при анализе программного кода из-за наличия циклов, ветвлений, псевдонимов и других конструкций, усложняющих код. Обычная практика для синтаксических анализаторов - использование набора эвристик для определения состояния гонки. Эвристики хорошо работают на элементарных тестах и модельных задачах, но показывают очень плохие результаты на реальных задачах.

В модели исполнения алгоритма в нескольких потоках сделана попытка учесть все возможные варианты исполнения путем введения «не коммутирующих» операций и классификации вариантов совместного исполнения на их основе. Для определенных задач анализ модели исполнения позволяет свести к нулю возможность ошибки false-negative (что очень важно). Однако, класс задач, для которых метод так хорошо работает, довольно узок. В работе предложено расширение модели, позволяющее значительно расширить класс анализируемых программ.

Анализ значений переменных.

Возьмем алгоритм взаимного исключения Петерсона. Критическая секция является таковой за счет проверки значений переменных, ограничивающих исполнения для всех потоков, кроме того, что находится в критической секции. Если статический анализ не включает контроль значений, то критическая секция с точки зрения такого анализа не является критической. В общем случае, задача

контроля переменных равносильна полноценному исполнению программы и вычислению значений всех переменных.

Четвертая глава

В четвертой главе автором предлагается и обосновывается расширенный подход к статическому анализу практических (не модельных) задач, включающий специфическую терминологию и методы.

Предлагаемое расширение модели

Гонка (в терминах графа в) - существование двух разных полных путей, для которых в финальной вершине состояния хотя бы одной из ячеек памяти различны. С учётом начальных значений ячеек и того, как их значения меняются, используем метод неопределенных коэффициентов. На каждом ветвлении добавляем коэффициент а е {0,1} к изменению в левой ветви и (1-я) - в правой. Множество неопределенных коэффициентов Б полностью описывает путь на графе. В финальной вершине имеем множество значений, где каждая ячейка памяти в общем случае имеет вид:

где х0 — состояние всех ячеек памяти в начальной вершине, О — значения неопределенных коэффициентов, / - некоторая функция, определенная для каждой из ячеек. Исходя из определения понятия гонки и принципов построения и анализа графа, изложенных выше, получаем, что гонка возможна тогда и только тогда, когда

где D|HD2- множества бинарных коэффициентов. Анализ таких обыкновенных конструкций кода, как ветвления и циклы, составляет сложность с точки зрения подхода, так как они добавляют на ребро графа совместного исполнения потоков дополнительные переходы. Например, простое ветвление типа if-else добавляет новый переход из одной вершины в другую, а цикл - добавляет переход назад. Несложно увидеть, что конструкция for - композиция перехода назад и условного ветвления.

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

Ветвления.

Простейшее ветвление, которое можно представить — одиночный оператор if следующего вида: if (condition) {operation;}. Отметим, что одна из идей построения графа совместного исполнения потоков - однозначное отображение один в один инструкций исходного кода на вершины на периметре графа. Именно такое построение обеспечивает линейную по набору инструкций сложность по каждому потоку. В случае простейшего ветвления имеется набор операций,

(2)

3/,Д,А:/Дх0,Д)*/ДХ0,£>2)

(3)

которые могут выполняться в зависимости от выполнения условия condition. Используя принцип неопределенных коэффициентов, будем считать, что набор операций operation выполняется, если равно 1 и не выполняется, если j> равно 0.

Например, в двух потоках исполняется следующий код при начальном значении х = 0:

if (х == 0) {

х += 2;

}

С точки зрения графа он будет иметь вид ребра, на котором значение х меняется на величину 2/?. Итак, в финальной вершине графа G значение /'той переменной равно f, (х0 ,D,B); где В - множество коэффициентов /?. Анализ на предмет наличия гонки проводится с неопределенными коэффициентами В полностью аналогично анализу коэффициентов D. В вершине графа ставятся значения разделяемых переменных, в ребра подписываются операцией, которой ребро соответствует. Для рассмотренного примера получили значение разделяемой переменной (в виде арифметического выражения) 2'/?,+2'/к Коэффициенты в выражении определяют ветвь, для которой моделируется исполнение. Существуют такие значения неопределенных коэффициентов, при которых разделяемая переменная принимает различные значения, то есть присутствует неразрешенное условие гонки.

Коэффициенты D отвечают за очередность исполнения операций, а В - за ветвления. В общем случае любое ветвление является композицией элементарных ветвлений. Также необходимо заметить, что в случае одиночного if в финальное выражение коэффициент [i может войти как множитель, что говорит о вариативности исполнения кода под условием. В случае конструкции if - else в финальное выражение войдут члены с коэффициентами /? и (1 -/?), отражающие тот факт, что выполняться будет либо блок кода под if, либо - под else. Корректность описанного представления докажем в следующей теореме.

Теорема 1. Наличие гонки в предлагаемой модели с ветвлениями эквивалентно наличию гонки в задаче (другими словами: предложенное выше представление корректно описывает ветвление в терминах и смысле анализа графа совместного исполнения потоков).

Доказательство. Рассмотрим множество фиксированных значений коэффициентов В в формуле f„ при этом анализируется линейный участок кода (пути по ветвлениям заданы множеством В). Наличие гонки в предлагаемой модели описывается формулой (3) с учетом коэффициентов Р так:

Ж и : /, (Х0 /; (х0 ,D2, В)

{0}

{2Р,+2Р2}

Рис. 2. Граф совместного исполнения двух.

В терминах исполнения алгоритма это означает, что есть такие два пути по ветвлениям, которые дают разные значения разделяемой переменной номер ¡. Таким образом, из состояния гонки в модели следует наличие гонки в алгоритме.

Обратно: путь есть такие два пути по ветвлениям алгоритма, которые приводят к гонке. В соответствии с формулой (3)

3/,£)1,£2 :/Дх0,Ц)^/Д.х0,£)2). Оба этих пути описываются с помощью множества коэффициентов В. Таким образом, наличие гонки в модели эквивалентно наличию гонки в алгоритме.

Циклы.

Исходная задача с циклами несколько сложнее, потому что циклы подразумевают переходы назад, а анализ графа совместного исполнения потоков - нисходящий. Таким образом, нет формального описания анализа циклов. Введем формальное правило анализа цикла и докажем его корректность с точки зрения поиска гонок.

Теорема 2. Для описания цикла в анализирующем графе достаточно одного повторения тела цикла.

Доказательство. Доказывать будем от противного. Допустим, необходимо повторение тела цикла два раза для того, чтобы обнаружить наличие гонки, которое бы не обнаружилось при проходе тела цикла один раз. Рассмотрим рисунок 3, приведенный ниже. На рисунке 3 жирной линией обозначен произвольный путь на графе. По предположению два подобных этому пути приводят к гонке, тогда как никакие два из путей в графе с одним повторением тела цикла к гонке не приводят. Рассматриваем отдельно каждый подграф, соответствующий одному повторению тела цикла и учитываем, что в нём гонка отсутствует.

остальной код

остальной

тело цикла у ч код

Рис. 3. Представление графа с несколькими повторениями тела цикла в виде подграфов с одним повторением в каждом.

Поскольку в анализе используются только попарные сравнения, а не последовательность использования операций, то из отсутствия гонки в каждой из подзадач следует отсутствие гонки в общей задаче, что противоречит исходному

п

предположению. Таким образом, предположение о том, что надо повторять граф совместного исполнения с повторением более, чем одного раза тела цикла, неверно. Обобщаем на случай п > 2 повторений тела цикла: обращаем внимание на то, что рассуждения выше не зависели от количества повторений цикла. Отметим, что при замене цикла на графе телом цикла, исчезают обратные переходы, что позволяет воспользоваться разработанным ранее подходом.

Разберём простейший пример применения подхода. Пусть в двух потоках исполняется следующий код:

\\'ЬПе(1гие) {

¡Ц1==0){ 1= 1;

else

break;

}

Исходные значения: х = 0, i = 0. Оставляем тело цикла и приписываем каждому из ветвлений коэффициент. Строим граф совместного исполнения потоков и отмечаем на нём операции чтения и записи. Рассмотрим путь, в котором потоки исполняются по очереди по одной инструкции, и выписываем значения разделяемых переменных с помощью метода неопределенных коэффициентов: i = 0ti, х = di + Cb,

откуда при aj = a2 = 1 получим значение х, при котором функция корректности имеет значение false. Значит, состояние гонки присутствует отностельно переменной х.

Общее представление о расчетном графе

Определение. Расчетный граф — конструктивная дискретная модель исходного кода программы, представляющая собой направленный граф, в котором каждому ребру соответствует атомарная операция, а вершинам ставится в соответствие множество значений всех разделяемых переменных. Пусть в графе выделена начальная и конечная вершины, соответствующие начальному состоянию переменных перед исполнением и конечному — после исполнения. Проход по графу моделирует один из вариантов совместного исполнения нескольких потоков путем точного указания следования инструкций одна за другой.

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

true,x = 1 false,х Ф1

(4)

х — состояние системы, а ./ — вектор-функция, показывающая, как меняется состояние системы после прохода по ребру. Определим на этом графе также функцию условного перехода:

М :ЩУ/1)^Р(х) = 0^ (6)

где Р — функция, определенная на множестве значений вектора разделяемых переменных. Это предикат, определяющий возможность передвижения системы из текущей вершины по рассматриваемому ребру, что соответствует условным переходам в программном коде.

Обозначение на рисунках и схемах

Значения всех разделяемых переменных будем обозначать на графе в фигурных скобках: {01}. Если Дл) меняет значение переменной, то в вершине, куда ребро ведет, новое значение будет подчеркнуто: {01}. Каждой атомарной операции соответствует одно ребро (так же, как и в графе совместного исполнения потоков). Отдельно можно выделить специальный вид ребер — ребра условия. Они содержат пустую операцию над переменными: и функцию-предикат Р(х), определяемую содержанием условия цикла (или содержимым обычного ¡0. Такие ребра появляются, когда в программном коде есть ветвления. Условие прохода по ребру определяет достижимость вершин, куда ребро ведет.

Представление циклов и ветвлений

Линейный программный код (без ветвлений) отображается на ребро графа без каких-либо дополнительных действий. Операции чтения соответствует ребро с Р з 1 и, возможно, нетривиальным предикатом Р(х), если речь идет, например, о конструкции ¡Г (л- == 1). При появлении нелинейных участков, таких, как циклы и ветвления, анализ усложняется. Будем использовать для представления ветвлений неопределенные коэффициенты (3 (аналогично коэффициентам а). Каждой из ветвей приписывается свой коэффициент, и только один из них равен 1, остальные — 0. На выходе имеем выражение с неопределенными коэффициентами, представляющее собой состояние системы на выходе из ветвления. Коэффициенты в выражении определяют ветвь, для которой моделируется исполнение. Обратных ребер в расчетном графе нет. Вместо них у ребер, входящих в тело цикла, появляется зависимость от параметра — номера итерации в цикле. Не всегда зависимость от номера итерации может быть задана явно, однако для реальных задач она, как правило, именно явная. Дополнительное условие налагается на систему условием выхода из цикла. Исходный цикл приобретает форму нескольких однонаправленных ребер, представляющих тело цикла, что, безусловно, облегчает задачу анализа.

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

13

разделяемыми переменными - линейны, т.е. все выражения содержат переменные в виде ® качестве примера можно привести операцию записи в

разделяемую переменную «х, = 2хг + 4 + х,» и операцию чтения разделяемых переменных «if(x1 = 3 & &2ху +3 = 5)».

Класс довольно широк: как показывает практика, в него входят (или сводятся) почти все действительные многопоточные алгоритмы.

Конструктивное построение расчетного графа

Построение расчетного графа аналогично построению графа совместного исполнения потоков. Как и в случае расчетного графа, вершины представляют собой состояния системы, отличающиеся друг от друга на одну атомарную операцию чтения/записи, а ребра соответствуют самим атомарным операциям. Отличия от графа совместного исполнения потоков заключаются в данных, сопоставляемых вершинам и ребрам. Каждому ребру соотносят функции (5) и (6). Для определенности будем подразделять ребра на два вида: ребра условия, где Р — нетривиальна, / — тривиальна и ребра операций, где Р — тривиальна, / — нетривиальна. Проход по такому графу из начальной вершины в конечную однозначно определяет последовательность взаимного выполнения инструкций двух потоков. Построение расчетного графа для п потоков полностью аналогично.

Расчеты на графе

После того как расчетный граф, состоящий из ребер операций и ребер условий, построен, и начальной вершине соотнесено множество исходных значений разделяемый переменных, можно приступать к расчетам. Каждая из итераций — проход по одному из путей из начальной вершины в конечную. В общем случае число путей достаточно велико — Будем рассматривать только те пути, которые были отобраны с помощью классов эквивалентности на графе совместного исполнения потоков. Таких путей значительно меньше — 0(п~к).

Поток 1:

Al: v = 1

А2:2 = 0

A3: while(x=I&&z=0);

А4: // critical section

А5:у= 0

Поток 2:

В1:л= 1

В2: z = 1

ВЗ: while(y=l&&z=l);

В4: // critical section

В5: х = 0

{000}

Рис. 4. Расчётный граф для алгоритма Петерсона.

¡000}

Элементарная часть итерации — проход их текущей вершины по ребру в следующую в соответствии с выбранным путем и затем либо изменение вектора состояния, либо проверка условия достижимости и проход по ребру (или признание ребра недостижимым). Если в графе были ветвления, то ребра, соответствующие ветвям цикла, будут иметь коэффициент /? и (1-Д). Коэффициенты войдут в выражение для значений переменных в финальной вершине. В зависимости от рода задачи и функции корректности по графу делается вывод о недостижимости критической секции, присутствии состояния гонки для конкретной разделяемой переменной и других подобных условий. Рассмотрим анализ алгоритма Петерсона в качестве иллюстрации применения предлагаемого подхода (рис. 4). Внутренние ребра намеренно не подписаны, но подразумевается, что расчеты производятся и для них тоже.

Рассмотрим путь, выделенный жирным, и вершину А на нем. Может ли система пойти из этой вершины по правому ребру? В вершине />" значение вектора состояния {1 10}. Условие попадания из Р в А — выполнение предиката у = 0 || ъ = 0. Если предикат верен, ребро, входящее в А, достижимо. Достижимость ребра А5' определяется предикатом х = 0 || 2 = 1. При векторе состояния {1 10} значение предиката ложно, поэтому ребро недостижимо.

Доказательство корректности подхода

Лемма. У путей, принадлежащих одному классу эквивалентности, порядок операций с любой разделяемой переменной - одинаков.

Это означает, что если взять всё множество последовательностей операций, соответствующих всем путям одного класса эквивалентности, выбрать любую из разделяемых переменных и посмотреть на порядок следования операций, совершаемых с этой переменной, то окажется, что порядок операций с этой переменной всегда одинаков.

Доказательство. Рассмотрим произвольный граф совместного исполнения потоков и произвольный класс эквивалентности этого графа. На рис. 3 приведен пример такого графа. Знаком «+» обозначены ячейки графа, образованные ребрами с не коммутирующими операциями, жирными линиями — класс эквивалентности. Доказывать будет от противного. Выберем класс эквивалентности, два пути на нем и некоторую разделяемую переменную.

Предположение: допустим,

порядок операций с этой переменной для выбранных путей - различный.

Обратим внимание, что в конечной вершине все операции так или иначе будут выполнены, значит, имеет место перестановка операций чтения/записи. Значит, состоялась одна из трех перестановок: 1) 2) 3) 15

Рис. 5. Положение класса эквивалентности относительно коммутирующих ячеек.

Первый вариант нас не интересует т.к. в обоих потоках происходит считывание значения переменной, и случай для нас неразличим. Рассмотрим перестановки 2 и 3. В них очередность исполнения явно влияет на содержимое разделяемой переменной. Обратим внимание, что местами могут меняться только операции из разных потоков, внутри одного потока порядок зафиксирован («порядок выполнения программы»). Значит, существует ячейка с ребрами W и W/R, каждое из которых входит в состав класса эквивалентности. Но такая ячейка является не коммутирующей, что исключает возможность её принадлежности к одному классу эквивалентности. Предположение не верно, порядок следования операций - одинаковый.

Теорема 3. Для того чтобы сделать вывод о наличии или отсутствии состояния гонки посредством анализа значений разделяемых переменных на введенном классе алгоритмов, достаточно рассмотреть представителей классов эквивалентности из графа совместного исполнения потоков.

Доказательство. При наличии единственной разделяемой переменной утверждение теоремы прямо следует из доказанной леммы. В ситуации, когда есть несколько разделяемых переменных, утверждение теоремы не очевидно и требует дополнительного доказательства. Далее предлагается доказательство от противного.

Пусть существуют два пути, принадлежащие одному классу эквивалентности, приводящие к различным значениям разделяемых переменных. Допущение сформулировано, используя отрицание формулировки теоремы и исходя из приведенного выше определения понятия гонки. Из доказанной леммы и различия значений переменных после исполнения следует, что существует некая строчка исходного кода или полученная по ней инструкция платформы, которые приводят к разным значениям одной из переменных. Это может быть либо явное присваивание переменной нового значения, например:

shared_x = fiinc(shared_y, shared_z);

либо логическое ветвление кода, приводящее к той же записи в переменную:

if (shared_y == 0) shared_x = 1;

else

shared_x = 0;

В любом из случаев на значение разделяемой переменной влияют значения остальных разделяемых переменных.

Вернемся к сформулированному выше допущению: предполагаем, что проход по разным путям в графе приводит к различным значениям переменных после исполнения программы. Отметим, что исходные значения разделяемых переменных не зависят от пути на графе совместного исполнения потоков. К интересующему нас моменту ветвления или записи значения переменных одинаковы для обоих потоков. Это следует из доказанной ранее леммы для каждой из переменных и из того факта, что до этого никаких ветвлений и записи

не было. Если ранее были ветвления или запись, то повторим доказательство для этого предыдущего ветвления или записи.

Но если значения всех переменных к моменту ветвления или записи одинаковы, то и результат соответствующих операций сравнения и записи будет одинаковым, следовательно, предположение о том, что для разных путей на графе в результате исполнения получаются разные значения, неверно.

Обоснованность использования представителей класса эквивалентности в расчетном графе.

Воспользовавшись доказанной теоремой 3, получаем одинаковую очередность операций с разделяемыми переменными в рамках каждого класса эквивалентности. Можно рассматривать это так, что каждый из потоков получает управление строго в определенный момент, когда это повлияет на дальнейшее исполнение программы, и до момента следующей развилки исполняется «в одиночестве» и так до момента выхода на не коммутирующие ячейки. Используяю этот факт, сложность анализа программного кода можно существенно сократить, взяв по одному пути из каждого класса эквивалентности. С учетом того, что классы эквивалентности покрывают все возможные пути, заключаем, что анализ представителей классов в расчетном графе дает ответ на вопрос о наличии гонок в алгоритме.

Пятая глава

В заключительной пятой главе приведены аспекты практической реализации комплекса программ для анализа многопоточных алгоритмов, а также примеры работы прототипа для различных алгоритмов.

Комплекс программ для полуавтоматического анализа

Автором был разработан комплекс программ полуавтоматического анализа многопоточных алгоритмов на предмет наличия состояний гонки. Программный комплекс реализующий принципы, заложенные в расширенную модель. В качестве исходного материала анализа выступает текст программы, предполагаемый для запуска в многопоточном режиме. Кроме того, для соответствующего кода должен быть определен «регламент»: сколько потоков, какие функции доступны из каких потоков. Чтобы использовать разработанный метод, код должен быть преобразован в специальное промежуточное представление. Его можно сравнить объектными файлами, получаемыми после компиляции программы: в нем «зашита» информация о переменных, их область видимости, очередность исполнения. Получить такую информацию позволяет Phoenix Toolkit, этот инструмент дает доступ ко всем сущностям программы в виде объектов. При помощи Phoenix Toolkit можно получить формализованное промежуточное представление программы из исходного кода.

Рис. 6. Комплекс программ для статического поиска состояний гонки в многопоточных алгоритмах.

Результатами обработки в Phoenix Toolkit является промежуточное представление программы. Важно заметить, что представление для языка С++ формируется с помощью Phoenix Toolkit, но оно может быть получено и с помощью другого программного инструментария. Могут быть проанализированы другие языки - лишь бы нашелся нужный разборщик, работающий подобно компилятору и позволяющий использовать результаты компоновки. Следующий шаг анализа - подача промежуточного представления на вход анализатору, прототип кода которого написан в Mathematica. С помощью разработанных методов строится граф совместного исполнения потоков, выделяются классы эквивалентности, представители классов, затем - расчетный граф и анализ путей на нем. Визуализация результатов так же часто выполнена в программе Mathematica: отображаются возможные способы исполнения и выводятся значения разделяемых переменных после исполнения.

Модельные эксперименты.

1. Алгоритм Петерсона.

Текст алгоритма Петерсона приведен на рис. 4. Вершина графа совместного исполнения потоков, соответствующая ситуации, когда оба потока оказываются в критической секции, обозначена буквой S на рис. 7.

ЧАЛ

ч/

Рис. 7. Допустимые классы эквивалентности и их представители для алгоритма Петерсона.

Пунктиром обозначены классы эквивалентности, сдвоенными стрелками — представитель класса. Множество допустимых классов эквивалентности не содержит вершины S, поэтому алгоритм действительно реализует критическую секцию. Сложность алгоритма по числу операций - 0(N3). Количество классов эквивалентности - 16, возможных вариантов исполнения - 4. Алгоритм корректен.

2. Стек Трейбера.

Стек Трейбера - неблокирующая реализация стека. Алгоритм и классы эквивалентности представлены на рис. 8. Имеем несколько серий решений:

Серии приведены для операции push в одном потоке и pop - в другом. Система получается в финальной вершине. Каждая серия соответствует одному из трех возможных вариантов взаимного исполнения потоков. Параметрами задано исходное состояние верхней ячейки стека. Решение каждой из систем приводит к одному и тому же значению ячейки стека.

{О, а} = (а, Ь} ар — (0, а}

top = {0,0}

({0,0} = (а, Щ [ top = £6,0}

PUSH(value) { node = new node(); node->value=value; node->next=NULL; repeat { top = GlobalTop; node->next=top; } until CAS(&GlobalTop, top, node)

POPO {

repeat {

top = GlobalTop; if (top==NULL) return; } until CAS(&GlobalTop, top, top->next)

/Оч /ÍAA Л/ЧАА

(XX, /Оу

\А/

✓Оч лаа

лААА кААУ

А. /ЧУХ.

\А/

/л/Ч/Ч ✓ \XV /Ч/Ч /V /Ч /ЧЛ

^ЛАА/у ЧЛ УЧ л/ V А. уч /

4V

ЛА

/ч/Ч /X Л, А/ , /Ч /Ч/\ ч/ /X /х/*»^ А V"4 х УДА/ \Л/

Ч -i

XXX

лАА>

ос ЧХ>

УЧл

ч А'

ОСа /

ч ч/

уОч

/XXX

Рис. 8. Стек Трейбера: классы эквивалентности и алгоритм.

Сложность анализа алгоритма стека Трейбера равна 0(N3+N2M~), где N -количество операций, М - количество условных конструкций в алгоритме. Количество классов эквивалентности - 6, возможных вариантов исполнения - 3. Алгоритм корректен.

3. Неблокирующая хеш-таблица.

Реализация неблокирующей хеш-таблицы с открытой адресацией описана в статье «Almost Wait-free Resizable Hashtables» авторами Gao, Groote, Hesselink. Далее приведен текст части кода добавления элемента в таблицу.

Будем анализировать ситуацию, когда два потока одновременно пытаются добавить элемент в хеш-таблицу. С точки зрения реализации хеш-таблицы, | корректный исход такого добавления - добавление обоих элементов в таблицу, а некорректный - перезапись элемента в таблице.

proc insert (v.Value \ {null}): Bool = local rEValue ;kl;nNat; h:pointer to Hashtable ; sue :Bool a:Address 27: a:=ADR(v);h=H[index]; 28: if h.occ >h.bound then newTable (); 30: h:=H[index]; fi 31: n0;l:=h:size ; sue :=false ;

repeat 32: k:=key (a;l;n); 33: <r: = h.tableffk];

{if a=ADR(r) then (iS) fi} > 35a: if oldp(r) then refresh (); 36: h:=H[index];

37: n:=0; l:=h.size ; elseif r=null then 35b: <if h.table[k]=null then sue :=true ; h.table[k]=v; {(iS)} fi> else n++ ;fi until sue || a=ADR(r); 41: if sue then <h.occ++ ;> ¡f 42:return sue

proc getAccess ()= loop

59: index :=cuiTlnd; 60: <prot[index]++ ;> 61 : if index =currlnd then 62: <busy[index]++ ;■> 63: if index =currlnd then return else releaseAccess (index);fi 65: else <prot[index]— ;> fi end end .

proc releaseAccess (i: 1.. 2P)=

local h:pointer to Hashtable ;

67: h:=H[i];

68: <busy[i]~ ;>

69: if h # nil Abusy[i]=0 then

70: <if H[i]=h then H[i]:=nil;>

71: deAllocate (h);fi fi

72: <prot[i]- ;>

end .

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

ч/ч

Ч/Ч/

/

Рис. 9. Представители классов эквивалентности для хеш-таблицы.

21

По результатам одновременного исполнения операции вставки в двух нитях в таблицу добавляются два элемента. Вставка корректна.

Авторы оценили сложность формального доказательства корректности всех операций с хеш-таблицей в два человеко-года. Сложность анализа работы алгоритма на операциях добавления элемента с помощью разработанного подхода по числу операций - 0(М3+М2М2), где N - количество операций, М - количество условных конструкций в алгоритме. Количество классов эквивалентности — 26, возможных вариантов исполнения-4.

В заключении приведены основные результаты работы и намечены направления дальнейшей работы.

ОСНОВНЫЕ РЕЗУЛЬТАТЫ РАБОТЫ

1. Разработана математическая модель исполнения многопоточных программ, учитывающая зависимость исполнения от начальных значений разделяемых переменных и позволяющая анализировать многопоточные алгоритмы, содержащие циклы, ветвления и атомарные операции.

2. Предложен метод полуавтоматического поиска состояний гонки (конкурентного доступа к памяти) в классе алгоритмов, содержащих только линейные операции с разделяемыми переменными, а также сформулированы критерии корректности для нескольких алгоритмов.

3. Создан комплекс программ для исследования многопоточных алгоритмов, содержащих циклы, ветвления и атомарные операции с целью выявления состояний гонки.

4. На основании результатов серии вычислительных экспериментов с использованием предложенной математической модели, методов и комплекса программ получены численные оценки сложности для ряда алгоритмов.

СПИСОК ПУБЛИКАЦИЙ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Заборовский Н.В., Тормасов А.Г. Моделирование многопоточного исполнения программы и метод статического анализа кода на предмет состояний гонки // Прикладная информатика - М.: 2011, №4(34). - С. 105110.

2. Заборовский Н.В., Тормасов А.Г. Расчетный подход к статическому анализу программного кода на предмет наличия состояний гонки // Программная инженерия - М.: 2011, №7. - С.46-54.

3. Заборовский Н.В., Тормасов А.Г. Статическое обнаружение гонок в коде, содержащем ветвления и циклы // Прикладная информатика - М.: 2011, №6(36). - С. 75-87.

4. Заборовский Н.В., Тормасов А.Г. Подход к нахождению состояния гонки в практических многопоточных программах // Сборник научных трудов

«Математические модели и задачи управления» - М.: МФТИ, 2011. - С. 198207.

5. Заборовский Н.В. Подход к моделированию вычислений в нескольких потоках // Сборник тезисов 5-й международной конференции им. П.Л. Чебышева- Обнинск: МИФИ, 2011. - С. 113.

6. Заборовский Н.В., Кудрин М.Ю., Прокопенко A.C., Тор.иасов А.Г. Автоматизация алгоритма поиска логических гонок в программах на разделяемой памяти // XXXVI Гагаринские чтения. Международная молодежная научная конференция. Научные труды. Т. 4. — Москва: МАТИ, 2010.-С. 91-92.

7. Заборовский Н.В. Моделирование функциональности системного реестра ОС Windows для использования в виртуализованных системах // Сборник тезисов XXXV Гагаринских чтений. - М. МАТИ: 2009. - С. 126-127.

8. Заборовский Н.В. Сборник тезисов XVI Международной научной конференции студентов, аспирантов и молодых учёных «Ломоносов-2009», секция «Вычислительная математика и кибернетика». - М.:МГУ, 2009 - С.

9. Заборовский Н.В., Шейнин В.В. Эффективная работа с данными при решении задач коллаборативной фильтрации // Сборник трудов VI Всероссийской конференции студентов, аспирантов и молодых ученых «Технологии Microsoft в теории и практике программирования» - М.:МГУ, 2009. — С. 13-15.

10. Заборовский Н.В., Петров В.Н., Разработка и реализация технологии шаблонного хранения данных в реестре Windows // Современные проблемы фундаментальных и прикладных наук. Часть VII. Прикладная математика и экономика: Труды XLIX научной конференции. /Моск. физ. - техн. ин-т. -М. - Долгопрудный, 2006. - С. 55.

11. Заборовский Н.В. Поиск состояния гонки в многопоточных алгоритмах // Современные проблемы фундаментальных и прикладных наук. Часть VII. Прикладная математика и экономика: Труды LIII научной конференции. /Моск. физ. - техн. ин-т. - М. - Долгопрудный, 2010. - С. 164.

12. Заборовский Н.В. Моделирование реестра ОС Windows для использования в виртуализованных системах // Сборник научных трудов «Модели и методы обработки информации» - М.:МФТИ, 2009. - С. 194-197.

В работах с соавторами лично соискателем выполнено следующее: [1,2,3,4] - разработка математической модели исполнения многопоточных программ и метода полуавтоматического поиска состояний гонки, создание комплекса программ и анализ ряда известных алгоритмов с целью выявления состояний гонки и получение для этих алгоритмов численных оценок сложности, [6,9,10] - описание поведения потоков в многопоточных приложениях при использовании средств синхронизации.

31-32.

Заборовский Никита Владимирович

РАСЧЕТНАЯ МОДЕЛЬ ДЛЯ НАХОЖДЕНИЯ СОСТОЯНИЙ ГОНОК В МНОГОПОТОЧНЫХ АЛГОРИТМАХ

АВТОРЕФЕРАТ

Подписано в печать 01.11.2011 Формат 60 х 84 1/16. Усл. печ. л. 1,0.

Тираж 70 экз. Заказ № 770. Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования «Московский физико-технический институт (государственный университет)» Отдел оперативной полиграфии «Физтех-полиграф» 141700, Московская обл., г. Долгопрудный, Институтский пер., 9

Оглавление.

Введение.

Актуальность темы.

Цель работы, задачи исследования.

Научная новизна.

Практическая ценность.

Положения, выносимые на защиту.

Публикации и апробация результатов.

Краткое содержание работы.

Глава 1. Обзор существующих методов.

Общие способы поиска проблем в параллельных программах.

Статический анализ.

Методы.

Типы анализа.

Алгоритмы.

Особенности работы.

Анализаторы.

Динамический анализ.

Методы.

Средства динамического анализа.

Проверка на основе моделей.

Синхронизация в многопоточных алгоритмах.

Неблокирующие алгоритмы.

Классификация исполнения параллельных программ.

Глава 2. Подходы к моделированию исполнения потоков.

Идея подхода.

Построение графа совместного исполнения п потоков.

Глава 3. Сложности и проблемы существующих подходов к моделированию исполнения потоков.

Проблемы современных систем статического анализа.

Ветвления.

Циклы.

Другие проблемы.

Анализ значений переменных.

Глава 4. Предлагаемая модель, ориентированная на реальные алгоритмы.

Предлагаемое расширение модели.

Ветвления.

Циклы.

Общее представление о расчетном графе.

Обозначение на рисунках и схемах.

Построение.

Метод неопределенных коэффициентов.

Класс анализируемых алгоримов.

Представление циклов и ветвлений.

Конструктивное построение расчетного графа.

Расчеты на графе.

Доказательство корректности подхода.

Обоснованность использования представителей класса эквивалентности в расчетном графе.

Глава 5. Практическая реализация анализа на построенной модели и результаты его работы на многопоточных алгоритмах.

Комплекс программ для полуавтоматического анализа.

Модельные эксперименты.

Выводы.

Актуальность темы.

Многопоточная организация программ достаточно давно применяется программистами. При одноядерной архитектуре процессоров использование нескольких потоков обеспечивало упрощение процесса программирования, работу с блокирующими операциями и. т.д. Чтобы эффективно использовать современные аппаратные платформы, нужны совершенно новые принципы и подходы. Под «эффективностью» понимается выигрыш от использования многоядерной платформы по сравнению. с> одноядерной. Иногда программы, написанные для одноядерной архитектуры, запускают на четырехядерной в надежде получить прирост производительности, а в результате оказывается, что производительность таких программ даже уменьшается.

Универсальных способов создавать эффективные программы!, не существует. Подход для каждой - строго индивидуален. Как одно из решений можно упомянуть неблокирующие алгоритмы -альтернативу алгоритмам, использующим явные средства синхронизации.

Отсутствие универсальных подходов влечёт за собой также возможные ошибки программистов. Одной из наиболее сложных для обнаружения ошибок является состояние гонки. Состояния гонки (race condition; конкурентного доступа к памяти) — ситуация, когда состояние общей для нескольких потоков ячейки памяти зависит от распределения процессорного времени между потоками. Предугадать это состояние на уровне алгоритма невозможно. Понять аналитически, что возникло состояние гонки, очень сложно, т.к. для этого требуется анализ экспоненциально растущего количества ситуаций. Именно поэтому так важно контролировать программы ещё на стадии описания. Создание средств контроля корректности программ становится всё более необходимым с выпуском каждого нового процессора и написанием каждого нового сложного программного комплекса.

Различают два принципиально разных подхода к анализу многопоточных алгоритмов на предмет наличия состояний гонки: динамический и статический. Динамический подход представляет собой эмпирическую процедуру «прогона» программы при различных входных данных (data-race-test в Google, Intel Thread Checker). Принципиальный недостаток подхода в целом невозможно проверить сложную систему, поскольку количество тестов экспоненциально зависит от числа- входных параметров. Статический подход анализирует архитектуру программы и программный код без его запуска. К статическому анализу относится формальное доказательство корректности кода программы. Для современных программных продуктов сложность формального доказательства значительна, что делает его неприменимым в промышленных масштабах. Кроме того, есть вероятность ложного срабатывания. Один и тот же алгоритм может содержать состояние гонки и не содержать его в зависимости от значений входных параметров.

В статическом анализе есть ряд известных проблем. В частности, многие алгоритмы используют в своей логике значения разделяемых переменных (алгоритм Петерсона[4], стек Трейбера[7]). Без учета значений при анализе таких алгоритмов получится заведомо неверный результат - это связано с тем, что логика поведения алгоритмов построена на проверке значений

разделяемых переменных. Большинству средств анализа алгоритмов не удается обнаруживать ошибки в логике алгоритмов, подобных алгоритму Петерсона. Поиск ошибок в таких алгоритмах- серьёзная исследовательская задача.

Отдельные задачи, неразрывно связанные со статическим анализом программ — задача об* идентификации разделяемых ресурсов и задача о превдонимах.

Помимо упомянутых методов, можно также отметить методы проверки на основе моделей (проверка, при которой варианты получаются из-модели, описывающей функциональность системы) и метод аналитического доказательства корректности [9] программ. Оба метода сложно применить на практике из-за того, что они занимают много времени и требуют больших человеческих усилий. Однако, иногда втречаются экзотические случаи их использования [27].

Цель работы, задачи исследования.

Существует несколько подходов к статическому анализу кода неблокирующих алгоритмов в поисках состояния гонки. Однако, большая часть из них носит чисто теоретический характер, подходит только для модельных задач и дает неточные результаты (большой процент ложных срабатываний и не обнаружений гонки, когда она есть, false-negative). Необходим подход к анализу исходных кодов современных прикладных программ, учитывающий их сложность и специфику.

Для этого, во-первых, необходимо разработать математическую модель, представляющую ход исполнения потоков с точки зрения работы с общими разделяемыми переменными. Модель должна быть применима для анализа реальных современных программ и моделировать исполнение современной многопоточной программы.

Во-вторых, на основе этой модели должен быть разработан метод, позволяющий:

• определять состояние гонки, если оно есть, не давая ложных срабатываний в определенном классе задач;

• давать результат за время, приемлемое для использования при тестировании программных продуктов внутри компании-разработчика.

Кроме модели и метода должен быть создан комплекс программ, анализирующий многопоточные алгоритмы с целью выявления состояний гонки и обладающий следующими свойствами:

• возможность анализировать исходный код на языках высокого уровня и выдавать промежуточное представление исходного кода, аналогичное тому, которое получается на стадии компиляции программы;

• реализация разработанного метода и указание мест возникновения гонки и приводящих к ней условий.

Научная новизна.

Научная новизна работы заключается в математическом моделировании поведения многопоточных алгоритмов, содержащих вервления и циклы, использующих разделяемую память. Математическая модель, предлагаемая в работе, учитывает начальные и промежуточные значения разделяемых переменных. Для модели разработана методика поиска состояний гонки в программном коде для определенного класса задач.

Хорошо известен ряд динамических и синтаксических анализаторов, обладающих следующими недостатками: тяжеловесность, зависимость от контекста, малая точность. Разработанный метод не зависит от контекста, определяет состояние гонки, если оно есть, и не даёт ложных срабатываний в рамках определенного класса алгоритмов. Что касается тяжеловесности, то для статических анализаторов эта проблема стоит менее остро, чем для динамических. В работе в качестве примера приведён легковесный алгоритм анализа.

Практическая г\енностъ.

Созданные модель и метод ориентированы на практическую реализацию. В работе предложены методика анализа кода на присутствие состояния гонки, использующая некое промежуточное представления кода, и техническая реализация получения промежуточного представления из исходного кода. В качестве средства обработки исходного кода может быть использовано любое другое подходящее средство, позволяющее получить специфицированное промежуточное представление.

Положения, выносилше на защиту.

1. Математическая модель исполнения многопоточных программ, учитывающая зависимость исполнения от начальных значений разделяемых переменных и описывающая, в том числе, такие конструкции программного кода как циклы, ветвления и атомарные операции.

2. Общий метод анализа многопоточных алгоритмов на предмет наличия гонок, в основе которого лежит анализ значений разделяемых переменных, и критерии корректности алгоритмов в понятиях разработанной модели.

3. Комплекс программ и результаты вычислительных экспериментов для выявления наличия гонок в некоторых многопоточных алгоритмах, в том числе неблокирующих.

Публикации и апробация результатов.

По теме диссертации опубликовано 12 работ, в том числе три [39, 40, 41] - в изданиях, рекомендованных ВАК РФ для опубликования основных научных результатов диссертаций.

Результаты работы докладывались и получили одобрение специалистов на научных семинарах и конференциях:

- XXXVI международная молодежная научная конференция «Гагаринские чтения» (Москва, 2009 г.),

- XXVII международные молодежные научные конференции «Гагаринские чтения» (Москва, 2010 г.),

- 5-ая международная конференция им. П.Л. Чебышева (Ногинск, 2011 г.),

- XVI Международная научная конференция студентов, аспирантов и молодых учёных «ЛОМОНОСОВ- 2009» (Москва, 2009 г.),

- 49-ая научная конференция МФТИ (Москва, 2007),

- 53-ая научная конференция МФТИ (Москва, 2009 г).

Краткое содержание работы.

Во введении обосновывается актуальность диссертации, и формулируются ее цели, характеризуются научная новизна и практическая ценность работы.

В главе 1 приводится краткий обзор существующих методов анализа исходного кода, а также программных средств, реализующих их.

Приводятся примеры статических анализаторов, приводятся известные проблемы и возможные пути решений. Рассматриваются такие анализаторы как Viva64, Intel thread checker, data-race-test, KISS, CHESS и другие.

В главе 2 описывается один из модельных подходов к описанию многопоточного исполнения алгоритмов, взятый за основу в данной работе.

В главе 3 излагаются сложности и узкие места при статическом анализе программного кода существующими методами. Рассматривается реальный практический код, часто имеющий сложную структуру, содержащий циклы и ветвления, а также атомарные операции.

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

В заключительной главе 5 приведены аспекты практической реализации комплекса программ для анализа многопоточных алгоритмов, а также результаты его работы на известных многопоточных алгоритмах с оценками сложности анализа.

Заключение.

1. Разработана математическая модель исполнения многопоточных программ, учитывающая зависимость исполнения от начальных значений разделяемых переменных и позволяющая анализировать многопоточные алгоритмы, содержащие циклы, ветвления и атомарные операции.

2. Предложен метод полуавтоматического поиска состояний гонки (конкурентного доступа к памяти) в классе алгоритмов, содержащих только линейные операции с разделяемыми переменными, а также сформулированы критерии корректности для нескольких алгоритмов.

3. Создан комплекс программ для исследования многопоточных алгоритмов, содержащих циклы, ветвления и атомарные операции с целью выявления состояний гонки.

4. На основании результатов серии вычислительных экспериментов с использованием предложенной математической модели, методов и комплекса программ получены численные оценки сложности для ряда алгоритмов.

1. Herlihy М., Shavit N. The Art of Multiprocessor Programming. Elsevier, 2008.

2. Serebryany K. Data race test Электронный ресурс. Режим дост.: http://code.google.com/p/data-race-test)3.|Qadeer S., Wu D. KISS: keep it simple and sequential. PLDI, 2004.

3. Peterson G. L. Myths About the Mutual Exclusion Problem // Information Processing Letters — 1981. -12(3). P. 1 15-1 16.

4. Bodden E., Havelund K. Racer: effective race detection using Aspectj. ISSTA, 2008.

5. Michael M., Scott M. Nonblocking Algorithms and Preemption-Safe Locking on Multiprogrammed Shared Memory Multiprocessors Электронный ресурс. — 1997. — Режим дост.:http ://f-cpu. seul. org/new/michae 19 8 nonblocking.pdf

6. Hendler D., Shavit N., Yerushalmi L. A Scalable Lock-free Stack Algorithm Электронный ресурс. — 2004. — Режим дост.: http://www.cs.tau.ac.il/~shanir/nir-pubs-web/Papers/LockFree.pdf

7. Патил Р. В., Джордж Б. Средства и приемы для выявления проблем параллельного выполнения Электронный ресурс. Режим дост.:-http://msdn.microsoft.com/ru-ru/magazine/cc5465 69.aspx

8. Карпов А. Тестирование параллельных программ Электронный ресурс. 2008. — Режим дост.: http://www.viva64.eom/ru/a/0031/

9. Романовский Е. Отладка многопоточных ОрепМР-программ // Мир ПК. 2008. - №02.

10. Herlihy М. Obstruction-Free Synchronization: Double-Ended Queues as an Example -Электронный ресурс. — 2003. — Режим дост.: http://citeseerx. is t. psu.edu/vie w doc/down load? do i= 1 0.1.1.83.7992&rep = repl &type=pdf

11. Skiena S. Combinatorics and Graph Theory with Mathematica 2004. — Электронный ресурс. - Режим до ст.: http://www.es .sunysb.edu/~skiena/talks/talk-combinatorica.pdf

12. Кудрин М.Ю., Прокопенко А.С., Тормасов А.Г. Метод нахождения состояний гонки в потоках, работающих на разделяемой памяти // Сборник научных трудов МФТИ. М.: МФТИ, 2009. - № 4. - Том 1. - С. 181-201.

13. О 'Callahan R., Choi J.-D. Hybrid Dynamic Data Race Detection PpoPP'03, San Diego, California, USA. - 2003.

14. Карпов А. Тестирование параллельных программ Электронный ресурс. — Режим дост.: http://www.softwaretesting. ru/library/testing/functionalte sting/5 8 1 -parallelprogramtesting

15. Savage S., Burrows M., Nelson G., Sobalvarro P., Anderson T. Eraser: A dynamic data race detector for multithreaded programs // ACM Trans, on Computer Systems. 15(4). - 1997.

16. Davies B. Whither Mathematics? // Notices of the American Mathematical Society. 2005. - V. 52, N.ll.

17. Emanuelsson P., Nilsson U. A Comparative Study of Industrial Static Analysis Tools // Elsevier Science Publishers. 2008. - Amsterdam, Netherlands.

18. Chelf В., Engler D., Hallem S. How to Write Systemspecic, Static Checkers in Metal // In PASTE '02: Proceedings of the 2002 ACM SIGPL AN-SIGSOFT workshop on Program Analysis for Software Tool and Engineering. 2002. P. 51-60.

19. Deutsch A. Interprocedural May-Alias Analysis for Pointers : Beyond k-limiting // In Proc. Programming Language Design and Implementation. ACM Press, 1994.

20. Sleensgaard B. Points-to Analysis in Almost Linear Time // In ACM POPL. 1996.

21. Калугин А. Верификатор программ на языке Си LINT Электронный ресурс. Режим дост.: http://www. viva 6 4 .com/go.php?url:=224

22. Карпов А. Что такое "Parallel Lint"? Электронный ресурс. — Режим дост.: http://software.intel.com/ru-ru/articles/par all el -lint/

23. Static Source Code Analysis Tools for C. Электронный ресурс. — Режим до ст. : http ://www. spinr о ot. com/static/

24. Gao H., Groote G.F., Hesselink W.H. Almost Wait-free Resizable Hashtables Электронный ресурс. — 2005. Режим дост.: http://www.cs.rug.nl/~wim/pub/hashtable.ps

25. Каличкин С.В. Обзор средств статической отладки. — Новосибирск: 2004. С. 12-22.

26. Terboven С. Comparing Intel Thread Checker and Sun Thread Analyze // Center for Computing and Communication RWTH Aachen University, Germany. -2007.

27. Использование Thread Analyzer для поиска конфликтов доступа к данным Электронный ресурс. — Режим дост.: http://ru.su п. com/de velopers/sunstudio/articles/thausin gru.html

28. Dinning A., Schonberg E. An empirical comparison of monitoring algorithms for access anomaly detection // In Proceedings of the Second ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP). 1990. - C. 1-10.

29. Mellor-Crummey J. On-the-fly detection of data races for programs with nested fork-join parallelis // In Proceedings of the 1991 ACM/IEEE conference on Supercomputing. ACM Press, 1991. - P. 24-33.

30. Perkovic D., Keleher P. Online data-race detection via coherency guarantees // In Proceedings of the 2nd Symposium on Operating Systems Design and Implementation (OSDI'96). 1996. - P. 47-57.

31. Ball T., Rajamani S. The SLAM project: debugging system software via static analysis // In Proceedings of the 29th ACM SIGPLAN-SIG ACT Symposium on Principles of Programming Languages (POPL'02). -ACM Press, 2002. C. 1-3.

32. Das M. Unification-based pointer analysis with directional assignments // In Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation (PLDI'00). ACM Press, 2000. - P. 35-46.

33. Chase D. R., Wegman M., Zadeck F. K. Analysis of pointers and structures. In Proceedings of the SIGPLAN '90 Conference on Programming Language Design and Implementation. 1990. - P. 296-310.

34. Orlovich M. On flow-insensitive points-to analyses Электронный ресурс. — Режим дост.:http://www.cs.cornell.edu/courses/cs7 1 l/2005fa/slides/s ер 1 3 .pdf

35. Кудрин М.Ю., Соколов Е.В., Тормасов А.Г. Выявление состояний гонки с помощью графа совместного исполнения потоков // Научно-технические ведомости СПбГПУ, Серия

36. Информатика, телекоммуникации, управление». — СПб.: Изд-во Политехи, ун-та, 2009. № 5 (83). - С. 125-134.

37. Заборовский Н.В., Тормасов А.Г. Моделирование многопоточного исполнения программы и метод статического анализа кода на предмет состояний гонки // Прикладная информатика — М.: 2011, №4(34). С. 105-110.

38. Заборовский Н.В., Торлгасов А.Г. Расчетный подход к статическому анализу программного кода на предмет наличия состояний гонки // Программная инженерия М.: 2011, №7. - С.46-54.

39. Заборовский Н.В., Тормасов А.Г. Статическое обнаружение гонок в коде, содержащем ветвления и циклы // Прикладная информатика — М.: 2011, №6(36).- С. 75-87.

40. Заборовский Н.В., Тормасов А.Г. Подход к нахождению состояния гонки в практических многопоточных программах // Сборник научных трудов «Математические модели и задачи управления»- М.: МФТИ, 2011. С. 198-207.

41. Кудрин М.Ю. Выявление состояний гонки с помощью графа совместного исполнения потоков // Материалы международной научно-технической конференции «Компьютерные науки и технологии» — Белгород: Изд-во БелГУ, 2009. С. 45-46.

42. Прокопенко A.C. Обнаружение состояний гонки в потоках, работающих на разделяемой памяти // Модели и методы обработки информации, сборник научных трудов М.: МФТИ, 2009. - С. 93-98.

43. Кудрин М.Ю., Соколов Е.В. Выявление состояний гонки с помощью аппарата атрибутных грамматик // Научное творчество молодежи. Материалы XIII Всероссийской научно-практической конференции. -Кемерово: Кемеровский гос. универ-т, 2009. — С. 112.

44. Purcell С., Harris Т. Non-blocking hashtables with open addressing. University of Cambridge, 2005.

45. Intel Architecture Software Developer's Manual. -Volume 1- 3 Электронный ресурс. Режим дост.: http ¡//download .intel .с om/design/intarch/manuals/243 1 9 101.pdf

46. Klein P. N., Lu H., Netze R. Detecting Race Conditions in Parallel Programs that Use Semaphores. -Lecture Notes in Computer Science. Springer Berlin/Heidelberg, 2008.

47. Fraser K. Practical lock-freedom. University of Cambridge, 2004.

48. Slonneger K., Kurtz B. Formal syntax and semantics of programming languages. — Addison-Wesley, 1995.5 1. Серебряков В.А., Галочкин М.П., Гончар Д.P., Фуругян М.Г. Теория и реализация языков программирования. М. : МЗ Пресс, 2006.

49. Herlihy М. Impossibility and Universality Results for Wait Free Synchronization // Proceedings of the seventh annual ACM Symposium on Principles of distributed computing, 1988. - P. 276-290.

50. Заборовский H.B. Подход к моделированию вычислений в нескольких потоках // Сборник тезисов 5-й международной конференции им. П.Л. Чебышева — Обнинск: МИФИ, 2011. С. ИЗ.

51. Заборовский Н.В. Моделированиефункциональности системного реестра ОС Windows для использования в виртуализо ванных системах // Сборник тезисов XXXV Гагаринских чтений. — М. МАТИ: 2009. С. 126-127.

52. Заборовский Н.В. Сборник тезисов XVI Международной научной конференции студентов, аспирантов и молодых учёных «Ломоносов-2009», секция «Вычислительная математика и кибернетика». М.:МГУ, 2009 - С. 31-32.

53. Заборовский Н.В., Пепгров В.Н. Разработка и реализация технологии шаблонного хранения данных в реестре Windows // Современные проблемы фундаментальных и прикладных наук. Часть VII.

54. Прикладная математика и экономика: Труды XLIX научной конференции. /Моск. физ. — техн. ин-т. — М.- Долгопрудный, 2006. С. 55.

55. Заборовский Н.В. Поиск состояния гонки в многопоточных алгоритмах // Современные проблемы фундаментальных и прикладных наук. Часть VII. Прикладная математика и экономика: Труды LIII научной конференции. /Моск. физ. — техн. ин-т. — М.

56. Долгопрудный, 2010. С. 164.

57. Заборовский Н.В. Моделирование реестра ОС Windows для использования в виртуализованных системах // Сборник научных трудов «Модели и методы обработки информации» М.:МФТИ, 2009. -С. 194-197.

58. Barnes G. A method for implementing lock-free shared data structures // Proceedings of the fifth annual ACM symposium on Parallel algorithms and architectures. — Velen, Germany, 1993. P. 261-270.

59. Gao H., Hessel ink W. H. A general lock-free algorithm using compare-and-swap. — Information and Computation, February, 2007. P. 225-241.

60. Herlihy M. A methodology for implementing highly concurrent data objects // ACM Transactions on Programming Languages and Systems (TOPLAS). November, 1993. P. 745-770.