Статический анализ гонок в программах на разделяемой памяти

• Автор: Прокопенко, Артем Сергеевич
• Шифр специальности: 05.13.18
• Научная степень: Кандидатская
• Год защиты: 2010
• Место защиты: Москва
• Количество страниц: 107 с.

Оглавление
Введение.

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

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

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

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

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

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

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

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

1.1. Обзор основных типов современных параллельных вычислительных систем.

Классификация параллельных архитектур
Современные направления развития параллельных вычислительных систем
Параллельные системы.
Взаимодействие потоков через разделяемую память
1.2. Состояние гонки
Методы синхронизации.
Синхронизация с блокировками.
Неблокирующаяся синхронизация
Транзакционная память
1.3. Обзор методов проверки правильности выполнения программ
Экспертиза.
Динамический анализ
Статический анализ.
Формальные методы
1.4 Классификация моделей.
Исполнимые модели
Ограничительные модели
Аксиоматические модели
Дополнительные виды моделей.
1.5. Классификация формальных методов
Методы проверки моделей.
Методы дедуктивного анализа.
Глава 2. Математическая модель.
2.1. Математическая модель.
2.2. Сепарационная логика
2.4. Синтаксис языка программирования
2.5. Операционная семантика
2.6 Утверждения. Формулы и аксиомы утверждений.
Глава 3. Метод верификации.
3.1 Обзор метода верификации Ле1уОиагап1ее
Комбинирование ИЛЗ и С8Ь
Метод ГЮ8ер и БАвЬ
Метод ЫЮ.
3.2. Переходы
3.4. Аксиомы и правила вывода
3.5. Доказательство непротиворечивости вывода
Глава 4. Спецификация формулы корректности.
4.1. Использование ЬТЬ логик для задания формулы корректности
4.2. Общая схема проведения анализа
4.3. Оценка сложности анализа на наличие гонок в параллельных программах
Глава 5. Примеры анализа многопоточных алгоритмов
5.1 Неблокирующаяся реализация алгоритма стека.
5.2. Неблокирующаяся реализация алгоритма очереди
5.3 Алгоритм булочной
Глава 6. Автоматизация.
8таГоог1Ш
Обзор среды каЬеНеНОЬ.
Описание комплекса программ
Заключение
Литература


Однако применение тех или иных механизмов синхронизации не является гарантией того, что не возникнет состояния неразрешенной гонки - ошибки многопоточного программирования, при которой выполнение программы нарушает ту часть спецификации (набор формализованных утверждений, описывающих требования к программе), которая касается доступа к общим данным. Поэтому необходима проверка правильности функционирования программы. В целом проверка соответствия между требованиями к системе и свойствами работающей системы (верификация) является нетривиальной задачей. Различают два принципиально разных подхода - динамический и статический. Динамическая верификация представляет собой эмпирическую процедуру «прогона» программы при различных входных данных. В итоге, несмотря на применение различных техник, отчетам динамических анализаторов свойственно большое количество ложных заключений о правильности программ. Проверка на основе моделей (model checking) и дедуктивная верификация, относящиеся к статическим формальным методам, реализуют статический подход альтернативный динамическому. Главными проблемами верификации на основе моделей являются сложность построения модели параллельных программ и «комбинаторный взрыв» в пространстве состояний системы, иначе говоря, значительный рост объема проверок даже при небольшом усложнении комплекса программ. В этом отношении выгодно отличается дедуктивная верификация, когда посредством формальной логики устанавливается соответствие результата выполнения программы представленной спецификации. Метод R/G- • Rely/Guarantee (Jones, )[] зарекомендовал себя как качественный метод верификации параллельных программ, когда спецификация параллельных программ может быть разбита на отдельные свойства, описывающие поведение небольших фрагментов системы, и может быть применима стратегия проверки каждого локального свойства, используя только тот _ фрагмент системы, который описывается лишь этим свойством. Допустим, что имеются п потоков Т|,Т2,. ТП, исполняющихся одновременно. Поскольку поведение потока Т! Rely), которые должны выполняться . Tj. Поведение среды также зависит от поведения потока Т], пользователь формулирует ряд допущений (Guarantee), которые должны выполняться потоком, для того чтобы гарантировать корректность выполнения среды. Однако посредством оригинального метода R/G можно проводит анализ наличия гонок лишь в простых типах программ (в программах без указателей, без локальной памяти потоков и т. В целях улучшения применимости метода R/G к верификации многопотоковых программ созданы три метода дедуктивной верификации: SAGL[], RGSep[5] и LRG []. Эти методы различаются как по математической модели, так и по типам программ, которые они способны верифицировать. Наиболее активно развиваются два: RGSep и LRG. Единственным серьезным преимуществом метода LRG перед RGSep является возможность верификации программ, в которых одни потоки имеют совместно используемые области данных, скрытее от других потоков. В прочих компонентах метод RGSep более проработан, это выражается в возможности верификации методом RGSep свойств живучести (живости, liveness). Он требует меньше усилий для . Для того, что нивелировать недостатки одного из методов, приходиться использовать оба. Сейчас, например, если необходимо проверить дедуктивным методом библиотечную функцию, создающую при выполнении несколько потоков, на отсутствие гонок, терм иру ем ость, то надо использовать и RGSep, и LRG, что фактически означает проведение двойной работы по спецификации, формальному доказательству (выводу последовательности формул). Целью диссертационной работы является создание метода статического анализа условий гонок многопоточных алгоритмов, основанного на RGSep-методе, для верификации параллельных программ, в которых некоторые потоки имеют совместно используемые области памяти скрытые от других потоков, а также проведение вычислительных экспериментов для исследования прикладных аспектов этого метода. Создание комплекса программ для автоматизации выявления совместно используемых потоками данных, декомпозиции «крупных» команд на атомарные инструкции.