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

004617395

Прокопенко Артем Сергееви^^^^^----

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

ПАМЯТИ

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

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

1 6 ДЕК 2010

Москва-2010

004617385

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

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

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

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

доктор физико-математических наук, профессор ДИКУ САР Василий Васильевич

кандидат физико-математических наук, доцент ПРОХОРОВ Сергей Петрович

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

Институт автоматизации проектирования РАН

Защита состоится декабря 2010 года в -—часов на заседании

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

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

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

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

Федько О.С.

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ Актуальность темы

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

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

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

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

Проверка на основе моделей (model checking) и дедуктивная верификация, относящиеся к статическим формальным методам, реализуют альтернативный динамическому статический подход. Главными проблемами верификации на основе моделей являются сложность построения модели параллельных программ и «комбинаторный взрыв» в пространстве состояний системы - значительный рост объема проверок даже при небольшом усложнении комплекса программ. В этом отношении выгодно отличается дедуктивная верификация, когда посредством формальной логики устанавливается соответствие результата выполнения программы представленной спецификации. Метод R/G - Rely/Guarantee (Jones, 1983) зарекомендовал себя как качественный метод верификации параллельных программ по заданным критериям. В этом методе для каждого потока выполнение параллельной программы представлено двумя отношениями: Rely и Guarantee, первое описывает изменение состояний, выполненное потоком, второе описывает результат всех других потоков - единой внешней среды (формальное описание метода Rely/Guarantee будет дано ниже). Однако, применение R/G - метода осложняется тем, что модель состояний представляется одним пулом памяти (нет разделения па локальные и общие состояния потоков). В результате необходимо целиком специфицировать состояния системы после каждого шага программы. Кроме того, метод не подходит для верификации свойства живучести (liveness properties) - т.е. свойства программ, которые утверждают, что нечто изначально задуманное произойдет при любом развитии внешних событий и любом ходе работы программы. Варианты частичного решения проблемы единого пула памяти предложены в методах RGSep (Vafeiadis, 2007) и SARG (Feng, 2007), в которых память разделена на локальную память каждого потока и общую для всех. Это позволяет не специфицировать абсолютно все локальные состояния выполнения программы. Сами методы являются синтезом R/G-метода и сепарациошюй логики (separation logic).

Также предложен способ использования метода RGScp для верификации свойств живучести (Gostman, 2009). Однако, модель в методах R/G, RGScp и подобных обладает следующими недостатками:

• несколько- потоков могут иметь совместно используемые ячейки памяти, скрытые от других потоков. В рамках методов R/G, RGSep, SARG нет возможности скрыть эти ячейки от других потоков, что может привести к ложному отчету о корректности программы;

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

Следует отметит, что синтаксис программ в RGSep включает «крупные» команды, многие из которых могут быть представлены несколькими операциями доступа к памяти (чтение/запись).

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

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

Задачи исследования:

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

2. разработка метода задания формулы частичной корректности, специфицирующей состояние гонки;

3. разработка метода анализа наличия гонок, используя расширение аксиоматического метода верификации Rely/Guarantee и сспарационной логики;

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

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

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

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

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

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

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

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

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

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

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

разделяемой памяти, в которых некоторые потоки имеют области общей

памяти, скрытые от других.

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

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

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

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

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

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

• IX международная научно-практическая конференция «Исследование, разработка и применение высоких технологий в промышленности» (Санкт-Петербург, 2010 г.);

• Международная научно-техническая конференция "Многопроцессорные вычислительные и управляющие системы 2009" (Дивноморское, 2009 г.);

• Седьмая международная научная молодежная школа «Высокопроизводительные вычислительные системы ВПВС-2010», (Дивноморское, 2010 г.);

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

• XLIX и L научные конференции МФТИ, (Москва, 2006, 2007 гг.);

• Научные семинары кафедры информатики МФТИ (Москва, 2008-2010 гг.).

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

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

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

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

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

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

В разделе 1.2 введено понятие гонки даппых(сЫа race), обобщенной roiiKH(general race). Обозначены современные подходы к синхронизации потоков: классические методы синхронизации (взаимоисключения, семафоры и т.д.), неявные методы cniixpomnaunn(iion-blocking structures), программная транзакционная naMATb(software transactional memory). Приведена известная теорема о консенсусе.

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

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

В разделе 2.1 приведено описание построенной модели. При самом моделировании параллельной программы использовалась широко распространенная предпосылка - чередование (мультипрограммное^, interleaving). Она позволяет в значительно упростить анализ реального параллельного вычисления, которое выполняется процессорами машины, и в тоже время адекватно его представить. Чередование позволяет представить выполнение параллельной программы, как последовательность дискретных шагов. Для того чтобы в таком представлении были учтены всевозможные сценарии исполнения программы, и при этом требование адекватного представления программы не нарушалось, необходимо чтобы инструкции были максимально атомарны. Отмечено, что на платформе архитектуры х86 гарантируется атомарность операции чтения, записи, и инструкции, реализующие примитив CAS(compare and swap). Сам выбор архитектуры х86 обусловлен ее широким распространением. Также нужно отметить, что в процессе оптимизации кода компилятор может переставлять фрагменты его местами для повышения производительности.

Пусть программа - это четверка (лis,s0,S,P'^, где Ms- множество общих ячеек памяти, s0eS- начальное состояние, ¿'-множество общих состояний, /-*'-конечньтй набор подпрограмм операций. Состояние — это отображение ячеек по множество значений.

Каждая подпрограмма Р" - это семерка

(ML,M,s,l„,L,v,T,<um подпрограммы >), где ML - множество локальных ячеек памяти, MslSMs - множество общих ячеек, доступных для подпрограммы ячеек, Iо - начальное локальное состояние, L - локальные состояния, Т = {/,,.. 1J -последовательность ассемблерных инструкций (команд) tj на архитектуре х86,

v:tJ - метки, = {ч0,-,чфш}. Локальные состояния подпрограммы не

доступны для других подпрограмм.

Для того чтобы, исполнить программу, надо задать потоки пользователя V = (рх,...,<рп. Каждый поток ^ представляет собой последовательность подпрограмм р1,...,р' . Поток стартует в начальном состоянии подпрограммы р', когда заканчивает ее выполнение, переходит в начальное состояние следующей подпрограммы и так далее.

Для заданных пользовательских потоков Ч' состояние выполнения характеризуется текущими значениями программных переменных а=(5,1',...,Г), где я - разделяемое состояние, /' - локальное состояние потока <р, и текущими метками у' всех потоков. Начальное состояние параллельной программы обозначим ст0 =(50,Множество состояний выполнения обозначим Само выполнение параллельной программы определяется как последовательность программных состояний а0,а1,а2,..., где каждое последующее состояние получено из предшествующего в результате соответствующего перехода (представляющее выполнение команды) одного из параллельных потоков: переход /',.../".../"; где ц(а)

обозначает, что выполняется операция с меткой ц в потоке ае Ч'.

Трасса выполнения программы - последовательность (.1|(а),Ц2(а),--4^(а) такая, что ст0—"||°|) хт, >....

Разделе 2.2 посвящен описанию базового языка программирования типа Си (определен синтаксис команд, описана модель программных состояний, операционная семантика, сепарационная логика).

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

инструкции до языка типа Си, а в самом методе вносятся соответствующие поправки.

Определен синтаксис команд программ следующим образом:

• выражения: Ф ::= Ф || Ф | Р;Р | Р;Р::= С\ Е | В;

• команды: С ::= skip \ х := Е \ х := [£] | [£]:=£ | С;С | if В then {С} else {С} | | while В do {С} | л: := newQ \ delele(E).

• целочисленные выражения: Е ::= х \ п \ Е iop Е;

• логические выражения: В ::= Ъ \ Е bop Е.

Вспомогательные определения: п е Z - множество целых чисел; beB = jtrue,false} - множество логических значений; iop е\ор = {+,-,[],...} -постоянное конечное множество целочисленных бинарных операций; bop е Во/? = {=,<,>,...} - постоянное конечное множество логических бинарных операций. Запись [х] означает содержание ячейки по адресу х. Оператор skip (пустой оператор) не меняет состояния программы.

Определено базовое понятие операционной семантики: состояние. В классических работах оно определяется как отображение программных переменных во множество их значений. Для того чтобы работать с программами, реализованными с помощью динамически выделяемых структур в работе используется сепарационная логика (separation logic). В этой логике множество программных состояний Е задаётся, например, следующим образом:

Values = {...,-2,-1,0,1,...}; Vars = {х,у,...,&х,&у,...}; Locations = {1,2,....}

Heaps = Locations —Values; Stores = Vars —> Values', X = Stores x Heaps

Поскольку в предложенной модели состояния могут быть одного из двух типов: локальные leL или общие seY., то программные состояния - это пары состояний (s,l) eS2.

Для привязки состояния к конкретной точке программы используется понятие конфигурации. Это пара <S, а> — программный фрагмент S и программное состояние а. После определены аксиомы и правила вывода

операционной семантики, описывающие бинарное отношение перехода во множестве конфигурации.

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

Пусть Е - пространство программных состояний, В - булево множество {0,1}, тогда утверждением р над пространством состояний называем предикат вида р = {а\а:1^В}.

Пусть р и q являются утверждениями в сепарационной логике:

p,q ::= false \етр \ е = е' \ е -> е\ р => q \ p*q | p-®q |... Здесь етр введено для обозначения пустой кучи (Heap), е-> «'описывает состояние, в котором куча состоит из одной выделенной ячейки по адресу е\ с содержанием е2. Оператор раздельной конъюнкции (separating conjunction) * является ключевым элементом сепарационной логики. Куча h удовлетворяет ФСП p*q, если ее можно разбить на две части, одна удовлетворяет утверждению р, другая q. Определение утверждения p*q вводиться через операцию • над £ такую, что для всех (li,hj),(h.hz) £

(t¡,hl.)»(t2,h2)-(tt,h¡ ±h2) , так что если t¡=t2 и \ lh2определено, иначе (,t¡,h¡)•

(t2,h2) не определено. И--- так, утверждение p*q:

(IГ, А) 1= (р * q) О ЭА..Л А, 1 h2 = h Л (ft, |= р) Л (h2 |= q).

Если для всех h¡,h, ,h2,h2 сА, таких что

tt i t

(h¡ lh2=h¡ lh2 \=р)л(1,/1, I = p) следует Л, = A, , то утверждение

Р = {а | а: Е -> В} называется однозначным утверждением precise(p).

Поскольку в предложенной модели состояния могут быть одного из двух типов: локальные/е2) или общие íeS, то ФСП характеризуют сразу и общие, и локальные состояние. Конечно, можно специфицировать каждое состояние посредством двух утверждений, но вместо этого воспользуемся грамматикой утверждений из RGSep. Тогда, пусть запись р - утверждение относительно

общих частей, а р — локальных.

Синтаксис: p,q ::= Р\Р\ р* q\ р Aq\ pv q\ p-®q .

12

Отношение |= выполнимости ФСП в состоянии (s,l) определяется по индукции:

(*,/)!=/> о/|=&„. р

(5,/)|=Р«(/=)Л(,|=^£ Р)

(Л О 1= А * Pi <=> 3/,, /2 (/ = /, X /2) л (Y,, s |=&Л, я,) Л <У2 - * К«,,/. Яг)

(i.')l=Pi Vft 0(/,,s|=&pi aM'j.sHs^ />2)

(s,/)|= p, лр, P,)A(/j,i P2)

(*,/)|=/>-®9оЭ/„/2(/2 =/, ±/)A(/„i|=^ p)A(/2,i|=Slpi q)

Здесь операторы определены на E2.

В главе 3 описаны метод верификации Rely/Guarantee, сделаны обзоры синтезированных методов: RGsep, SARG, LocalRG; описан предложенный автором метод анализа гонок на разделяемой памяти; введена формула корректности; доказана непротиворечивость предложенной логики.

Раздел 3.1 посвящен методу формальной верификации Rely/Guarantee: спецификация, система правил, приводиться теорема о непротиворечивости.

Суть метод формальной верификации Rely/Guarantee заключается в следующем: пусть заданы потоки Ч' = <р^,...,(рп, для всех ocf рассматривается выполнение программы. Другие потоки Ч',. = 'К \ {а} называются средой потока а. Спецификация выполнение потока а определяют четверкой (pre,R,G,post) где р-предусловие (утверждения, которые должны быть истинны в начале выполнения потока), ^-постусловие (утверждения, которые должны быть истинны после выполнения), G - спецификация шагов потока a, R -спецификация шагов среды но изменению данных в течение выполнения потока а. Далее посредством применения правил вывода проверяется, что выполнение потока удовлетворяет заданной спецификации.

Раздел 3.2 посвящен формализации переходов системы из одних состояний в другие.

В методе, предложенном автором, Rely и Guarantee условия определяют характер изменений общих состояний. Введено понятие deucmeuii(actions)

Р ~> д, которые определяют переходы между состояниями, специфицированными утверждениями р и д :

О (.5 = .?, = ^ Х^Л^,,.?,' |=°1)Л('У2>'?2 \~а')\

1=а=>а' <=> если из ж,|=а,следует |=а'.

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

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

Утверждение р устойчиво под действием а 51аЬ(р,а) тогда и только тогда, когда таких, что .v |= р л(л,х' \= а) следует л-' |= р.

Доказана лемма 1. г- >д) о | = (г-®р)*д=$р

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

Доказана лемма 2. (Л, иЯ2)*) <=> АяЛ(р,/?,)лЯшЬ(р,Я2)

Вторая лемма о том, что утверждение р устойчиво под множеством действии Я тогда, когда устойчиво под действием каждого.

Доказана лемма 3. $1аЬ(рх,а) л $1аЬ(р2,а) <=> Ла/^р, л р2,а);

51аЬ(р1, а,) V 1?/ай(/?2, о2) <=> БшН^р, V р2, а, л а2);

о,) л Йа6(Р> а2) <=> $1а1(р, а, л а2).

Казалось бы сепарационная конъюнкция над действиями а*а' позволит скомбинировать различные переходы в одну запись, однако это не так.

Пример. Пусть Ц н> 1, я, = {1.2н» 2, Ь2 (-> 3} и Ь2 4, аг = {Ц ^ 5,1Л 6} причем/,, ф Ь2, т.е. имеем ЯшЦр,,а),&1аЦр2,а) и Ая^р, *р2,а, *а2)ложь.

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

Говорят, что действие а защищено точным инвариантом I > а тогда и только тогда, когда инвариант имеет место в начальном и конечном переходах, удовлетворяющих а, и является точным инвариантом precise(I): а => (/ ~> 7) л precise(/).

Доказана лемма 4. (Sta/ip^aJ л Stab(p7,a2) л /?, =>/)л(/>а)о

oStab(Pi* p2,at *а2)

В разделе 3.4 представлена аксиоматическая система.

Выводимость модифицированной тройки Хоара обозначена как R\G\l\-{pre}C{post), что означает, что если предусловия удовлетворяют pre, изменения общих состояний выполняются в соответствии с R, выполнение кода потока удовлетворяет G при защите точным инвариантом /, и если подпрограмма завершает работу, то постусловия удовлетворяют post.

В работе введено понятие сепарационной конъюнкции для спецификации R,*R2, Gi*G2, инварианта 1*12, введено два новых правила вывода для скрытия части общих данных и «разбивки» локальных:

R-,G;l\-{P*Y}C{Q*Y'} Stab(M,R) I>{R',G'} M^>I'*true /т,

-1-=-==-=-^-(Frame)

R,G,l\-{P*Ms*Y)C{Q*Ms*r} v

R*R'-G*G,-,I*l,\-{p}C{g} / > {R,G} R,G,l\-{p}C{q)

В качестве примеров приведены следующие правила, типичные для R/G методов, но записанные в рамках предложенной системы:

R,G,l\~{pre}C{post] Stab(p, R и G))

R,G,l\-{pre* p]C{post * р} (Stab)

R',G',l\-{pre'}C{post'} RczR' C'cG pre => pre' post' => post

RtG,i\-{pre}C{poSt} (Weaken)

R; G; l\-{pre, }C{post} R; G; l\-{pre2}C{post}

R;G;l\-{pre, иpre2 }C{posl} (Dlsj)

tf ;G;/|-{pre}C{pos/,} R; G; j\-{pre}C{post2}

R; G; 1\-{рге}С1рач11 n Poi(2( (Conj)

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

Л о G2; G,; * Г}С, {0, * I > {R,G} R^G,;G1-,I\-{P2*DC2{QZ*'I\}

R-, G, и G2; /|-{Р, * Р2 * Т } С, || С2 {Р, * Р2 * (Л, л Л2)} (Раг)

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

P~>Q^G PkjQ^>1 1>{R,G} Sta({P,Q},R) Pt ~> & с G

/?; G; /j-{/> * P}atomic {C) {Q, * ¿>1 (Atom)

В разделе 3.5 определяется взаимоотношение между формализованным исчислением высказываний и алгеброй высказываний, между синтаксисом и семантикой, Для этого доказывается теорема о непротиворечивости для свойства частичной корректности.

В начале дается по индукции формализованное определение выполнимости спецификации G на пути исполнения программы Guar(G, С, a,R). Неформально, это звучит как: пусть программный код С начинает выполняться из состояния о, действия среды удовлетворяет спецификации R, тогда говорят, что выполнение потока удовлетворяет спецификации G, тогда и только тогда, программа не завершается аварийно и изменение всех общих состояний выполняется в соответствии с G.

Далее вводиться определение истинности формулы частичной корректности: R; G; 11= {p}C{q} о /,,ф p,Guar(G,C,(l,s),R),(С,(l,s))-*->*(skip, (/',«')),

lW\=q-

Доказана лемма 5. Если программный код С является примитивом, то возможен один из трех сценариев: (С,а)——>*(С",сг') <=> (С,ег)—*(С,сг');

(С, а) '—> * fault «](г'.(С,<7) —(С, а") —„ fault;

(С, a) -?->*(skip, а') о 3 а"а".(С, <т) —(С, а P(skip, (skip, сг').

Доказана лемма 6 об условии G при параллельном исполнении. Если

Guar(Gl,C,,c7,R<jG2), Guar(G2,C2,a,R<jG,) и сг, о<т2=<т, то

Guar(G, и G2, С, || С2, сг, Л); если (С, || С2, <т) —*(С[ || С2, сг'), то

3g,',g;.(C„<r,) >«(C,',g,'), (C2,ff2)^L>*(C>;), <r,,*o'1=o>.

Доказана лемма 7 об условии С при последовательном исполнении. Если Guar(G,С,, <т, Л), Vct' : (С,, <т) —^*(skip,a'), Guar(G,C2,a'Jt),то Guar(G,С,;С2,<т,Д).

Доказана лемма 8. Если (С,;С2,сг)—!—**(skip,a"), тогда

За'^.сг) —s-^*(skip,a') и (С2,<т') —>*(skip,а").

Для интерпретации выводимости как доказательства в смысле частичной корректности необходимо, чтобы система вывода обладала свойством непротиворечивости, т.е. чтобы при выполнении общезначимых формул получались общезначимые, что отражает следующая теорема о том, что предложенная система вывода непротиворечива для свойства частичной корректности: если R;G;l\-{p}C{p] то R;G;I\={p}C{p}. Программа считается прошедшей проверку, если для каждого потока, с помощью применение аксиом и правил, показан вывод формулы корректности. ■

Глава 4 посвящена способам задания формул корректности, приведены примеры задания формул, сделаны оценки сложности алгоритма анализа гонок.

В дедуктивных методах на основе Rely/Guarantee спецификация (R, G,

пред/постусловия) выполнения команд потока выражается посредством

задания формулами состояния памяти, для каждой логически законченной

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

меньшей выразительной способность, чем спецификации посредством

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

выраженной посредством временной логики LTL (Linear Temporal Logic) и

формулами R и G в методе R/G. Применение временной логики, изначально

приспособленной к рассуждению о последовательностях, к анализу

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

17

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

Синтаксис LTL включает в себя стандартные темпоральные операторы (X,F,G,U,R), булевы связки (-,, л, v) и пропозициональные переменные типа atl, которые пробегают по выражениям «поток <pt находиться в метке /».

Синтаксис ¿TL-формул таково:

• пропозициональные переменные atl;

• True, False;

• <pnyj- формулы, то: ^<р, <рЛу/, (pVy/- формулы;

Х<р, F<p, G<p, (pUijj, (pRy - формулы.

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

Пример. ОбщийЧ|юрмулы частичной корректности в логике LTL примет следующий вид: пусть (р - предусловие, а у/ - постусловие. Пусть f ¡, 1°2— 1°„-исходиые метки потоков параллельной программы Ti||...||T„ , Г/, Г2... Г„-консчные метки этих же процессов. Тогда частичная корректность данной программы относительно (р и у/ может быть выражена следующей формулой: (atl°i& ... atl°n & <р) => G(atf!l& ... а/Г„ & i//).. Что преобразуется в формулу частичной корректности в виде терминах троек Хоара {(р) Ti||...||Tn { у/ }. А общий вид формула частичной корректности одного потока в предложенном методе имеет вид R;G-,I\- {<р„\Тгх{у/а\.

Пример. LTL вид формулы корректности, которая описывает свойство исключения критической секции: f r> G-(atlx,...,atln), где ^-формула, выражающая исходные предусловия, //,.../„-метки входа в критическую секцию. В методеG-^ai/,,...,atln)\I\-{^}Та{true}, где G-оператор темпоральной логики LTL.

Получены оценки сложности алгоритма анализа. В частности, оценка числа правил и аксиом для одного потока - О(п), где п - число операторов

потока; оценка общего числа правил вывода для анализа всех к различных потоков программы: 0(n2kv), где v- число задействованных общих ячеек.

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

Рассмотрена неблокирующуяся реализация алгоритма стека.

Пусть:

class Node { Node * next; int data;};

void push(int t) {

Node* node = new Node(t); do {

node->next = head; } while (!cas(&head, node, node->next));

};

Пусть каждый поток представляет из себя последовательность подпрограмм void push() и в работе не рассматривается АВА-проблема, поэтому формула частичной корректности R,G,/| = {prejpus/г{post} имеет следующие составляющие:

• Инвариант I: 3x.&head -> х * lseg(x,NULL) * true, где lseg(x,y) <=> (х = у п

emp) U (3z.x * у П х -»,(*+!)-» у * lseg(z,yj).

• Предусловие pre:[head] -> у

• Постусловие post: [head] ->x*x->t*(x + l)->y

• Для определения R,G заметим, что запись происходит посредством

инструкции CAS. При условии равенства первых двух аргументов:

{[/lead] -» y)CAShead{[head] ->х*х->Г*0 + 1)->у}

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

Рассмотрена неблокирующаяся реализация алгоритма очереди.

Пусть определен массив int q[N] и две переменные int tail и int head. Здесь

N - некоторое заранее заданное число, а массив и переменные расположены в

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

переменная head содержит номер первого элемента в очереди, a tail - номер

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

Добавление элемента в очередь выглядят следующим образом:

boot Enqueue( int х ) { int t;

while (1) { Al: t=tail;

A2: if (t == N) return 0; A3: if (q[t] != NULL) { A4: CAS(tail, t, t+1);

continue;} A5: if (CAS(q[t], NULL, x)) { A6: CAS(tail, t, t+1);

A7: return 1;}

} }

В работе не рассматривается АВА-проблема, поэтому формула частичной корректности R,G,I\ = [pre}enqueue {post} имеет следующие составляющие: • Инвариант: Isegihead, tail) * tail -» Null

• Предусловие: Isegihead, n, tail) * tail -> Null

• Постусловие: (lseg(head,n + 1, tail) * tail -> Null * [n] -> x)u

U {Isegihead, n, tail) * [tail] -> N)

• Для определения R, G заметим, что запись происходит посредством инструкции CAS. При условии равенства первых двух аргументов CAS: {true}CAStni,{tail = tail + 1); lseg(head,n, tail) * [q + t] -»

-> Null] CASq[t\[lseg(head,n, tail) * [ta.it] -» x U lseg(head,n,tail) n ([<7 + t] = x)}

Для наглядности выполнение разбито ira типы проходов по циклу:

Типы проходов по циклу whilc(l) Guarantee Rely Rely/Guarantee

Терминация в А7 CAS *CAS all] tail Inv Inv

Термипация вЛ7 CAS altl CAS tail Inv

Терминация вА2 1 nv Rely 0 Inv *Rcly 0

Прогон по циклу без термипации Inv*CAS fäll Rely холостой Inv*CAS *Rely tail 1

Тогда выполнение программы удовлетворяет формуле корректности. В главе 6 представлен комплекс программ для автоматизации предложенного метода анализа гонок па общей памяти.

Для предложенного метода, как и для других аксиоматических методов, сложность автоматизации является одним из главных препятствий для широко применения. В целях автоматизации верификации программ в среде Isabella/HOL на базе генераторов Flex и Bison написан комплекс программа по автоматическому извлечению инструкции доступа к памяти, разложению операторов на атомарные, переводу выражений в постфиксную запись и т.п. В Заключении приведены основные результаты работы. ОСНОВНЫЕ РЕЗУЛЬТАТЫ РАБОТЫ

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

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

3. Предложен метод анализа параллельных программ на наличие гонок на основе расширения аксиоматического метода верификации Rely/Guarantee и сепарационной логики.

4. Оценена сложность алгоритма анализа гонок в параллельных программах предложенным методом.

5. Разработан комплекс программ для автоматизации предложенного метода анализа гонок.

6. Комплексно исследован ряд задач параллельного программирования на основе анализа их математических моделей с помощью предложенной методики и вычислительных экспериментов.

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

1. Прокопенко A.C., Тормаеов А.Г. Аксиоматический метод верификации на основе декомпозиции состояний в методе RGSep. // Научно-технические ведомости СПбГПУ, Серия "Информатика, телекоммуникации, управление." — СПб.: Изд-во Политехи, ун-та, 2010. — №6 (113).-С. 112-121.

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

3. Прокопенко A.C., Тормаеов А.Г. Синтез метода Джонса и сепарационной логики для дедуктивной верификации параллельных программ на наличие условий гонки // Высокопроизводительные вычислительные системы ВПВС-2010. Материалы Седьмой Международной научной молодежной школы. - Ростов-на-Дону - Таганрог, 2010. - С. 240-244.

4. Прокопенко A.C., Тормаеов А.Г. Дедуктивный метод анализа логических гонок с использованием сепарационной логики. // Труды МФТИ. — М., 2010. - Т.2. № 3. - С. 175-184.

5. Кудрин М.Ю., Прокопенко A.C., Тормаеов А.Г. Детектор логических гонок для программ, работающих на разделяемой памяти // Высокие технологии, исследования, промышленность. Сборник трудов девятой международной научно-практической конференции «Исследование, разработка и применение высоких технологий в промышленности». - С.-Пб, 2010.-С. 67-71.

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

7. Кудрин М.Ю., Петров В.Н., Прокопенко A.C., Тормаеов А.Г. Математическое моделирование структур, работающих на разделяемой

памяти // Материалы международной научно-технической конференции "Многопроцессорные вычислительные и управляющие системы 2009". -Таганрог: Изд-во ТТИ ЮФУ, 2009. - Том 1. - С. 73-74.

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

9. Кудрин М.Ю., Петров В.Н., Прокопенко A.C. Математическое моделирование структур, работающих на разделяемой памяти // XXXVI Гагаринские чтения. Международная молодежная научная конференция. Научные труды. Т. 4. - Москва: МАТИ, 2009. - С. 24-25.

Ю.Прокопенко A.C. Математическое моделирование структур, не требующих блокирования при параллельном доступе. // Современные проблемы фундаментальных и прикладных наук. Часть VII. Управление и прикладная математика: Труды 50-й научной конференции. - М.Долгопрудный: МФТИ, 2007. - С. 62-63.

11. Прокопенко A.C., Тарасов В.Н. Перспективы применения структур, не требующих синхронизации при параллельном доступе II Современные проблемы фундаментальных и прикладных наук. Часть VII. Управление и прикладная математика: Труды 49-й научной конференции. - М.Долгопрудный: МФТИ, 2006. - С. 50.

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

Прокопенко Артем Сергеевич

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

ПАМЯТИ

Автореферат

Подписано в печать 12.11.2010 Формат 60x90/16. Уел печ л 1.0. Тираж 90 экз. Заказ No 770. Московский физико-технический институт (государственный университет)

Печать на аппарате Rex-Rotary Copy Printer 1280. НИЧ МФТИ.

141700, г Долгопрудный Московской обл, Институтский пер, 9, тел.: (095) 4088430, факс (095) 5766582

Введение.

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

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

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

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

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

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

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

Глава 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ер и БАвЬ.

Метод 1Жт.

3.2. Переходы.

3.4. Аксиомы и правила вывода.

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

Глава 4. Спецификация формулы корректности.

4.1. Использование ЬТЬ логик для задания формулы корректности.

4.2. Общая схема проведения анализа.

4.3. Оценка сложности анализа на наличие гонок в параллельных программах.

Глава 5. Примеры анализа многопоточных алгоритмов.

5.1 Неблокирующаяся реализация алгоритма стека.

5.2. Неблокирующаяся реализация алгоритма очереди.

5.3 Алгоритм «булочной».

Глава 6. Автоматизация.

БтаПйкЛЯО.

Обзор среды ЬаЬеПе/НОЬ.

Описание комплекса программ.

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

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

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

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

Проверка на основе моделей (model checking) и дедуктивная верификация, относящиеся к статическим формальным методам, реализуют статический подход альтернативный динамическому. Главными проблемами верификации на основе моделей являются сложность построения модели параллельных программ и «комбинаторный взрыв» в пространстве состояний системы, иначе говоря, значительный рост объема проверок даже при небольшом усложнении комплекса программ. В этом отношении выгодно отличается дедуктивная верификация, когда посредством формальной логики устанавливается соответствие результата выполнения программы представленной спецификации. Метод R/G-Rely/Guarantee (Jones, 1983)[68] зарекомендовал себя как качественный метод верификации параллельных программ, когда спецификация параллельных программ может быть разбита на отдельные свойства, описывающие поведение небольших фрагментов системы, и может быть применима стратегия проверки каждого локального свойства, используя только тот фрагмент системы, который описывается лишь этим свойством. Допустим, что имеются п потоков Ti,T2,.Tn, исполняющихся одновременно. Поскольку поведение потока Ti зависит от поведения других потоков, именуемых средой, пользователь 'формулирует ряд допущений (Rely), которые должны выполняться средой, для того чтобы гарантировать корректность потока Ti. Поведение среды также зависит от поведения потока Ть пользователь формулирует ряд допущений (Guarantee), которые должны выполняться потоком, для того чтобы гарантировать корректность выполнения среды. Построив должным образом комбинацию допущений потоков, можно установить правильность всей системы TijjT^H - - - j[Tn.

Однако посредством оригинального метода R/G можно проводит анализ наличия гонок лишь в простых типах программ (в программах без указателей, без локальной памяти потоков и т.д.). В целях улучшения применимости метода R/G к верификации многопотоковых программ созданы три метода дедуктивной верификации: SAGL[63], RGSep[105] и LRG[64]. Эти методы различаются как по математической модели, так и по типам программ, которые они способны верифицировать. Наиболее активно развиваются два: RGSep и LRG. Единственным серьезным преимуществом метода LRG перед RGSep является возможность верификации программ, в которых одни потоки имеют совместно используемые области данных, скрытее от других потоков. В прочих компонентах метод RGSep более проработан, это выражается в возможности верификации методом RGSep свойств живучести (живости, liveness). Он требует меньше усилий для верификации компонентов системы в различных окружениях за счет исследования устойчивости слабейших предусловии и слабейших постусловия под влиянием окружения; определенные шаги метода автоматизированы. Для того, что нивелировать недостатки одного из методов, приходиться использовать оба. Сейчас, например, если необходимо проверить дедуктивным методом библиотечную функцию, создающую при выполнении несколько потоков, на отсутствие гонок, термируемость, то надо использовать и RGSep, и LRG, что фактически означает проведение двойной работы по спецификации, формальному доказательству (выводу последовательности формул). Для того чтобы в подобных ситуациях использовать один метод, необходимо нивелировать ряд недостатков в методах R/G, RGSep, а именно:

• несколько потоков могут иметь совместно используемые ячейки памяти, скрытые от других потоков. В рамках методов R/G, RGSep, SARG нет возможности скрыть эти ячейки от других потоков, что может привести к ложному отчету о корректности программы;

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

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

Целью диссертационной работы является создание метода статического анализа условий гонок многопоточных алгоритмов, основанного на RGSep-методе, для верификации параллельных программ, в которых некоторые потоки имеют совместно используемые области памяти скрытые от других потоков, а также проведение вычислительных экспериментов для исследования прикладных аспектов этого метода. Задачи исследования:

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

2. Разработка метода задания формулы частичной корректности, специфицирующей состояние гонки;

3. Разработка метода анализа наличия гонок, используя расширение аксиоматического метода верификации Rely/Guarantee и сепарационной логики;

4. Оценка сложности алгоритма анализа гонок в параллельных программах на общей памяти в различных случаях;

5. Использование предложенного подхода и соответствующих вычислительных экспериментов для выявления состояния гонки в тестовых параллельных программах на разделяемой памяти;

6. Создание комплекса программ для автоматизации выявления совместно используемых потоками данных, декомпозиции «крупных» команд на атомарные инструкции.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

• IX международная научно-практическая конференция «Исследование, разработка и применение высоких технологий в промышленности» (Санкт-Петербург, 2010 г.);

• Седьмая международная научная молодежная школа «Высокопроизводительные вычислительные системы ВПВС-2010»,

• (Дивноморское, 2010 г.);

• Международная научно-техническая конференция "Многопроцессорные вычислительные и управляющие системы 2009" (Дивноморское, 2009 г.);

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

• XLIX и L научные конференции МФТИ (Москва, 2006, 2007 гг.);

• Научные семинары кафедры информатики МФТИ (Москва, 20082010 гг.).

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

Диссертация состоит из Введения, шести глав, Заключения и Списка использованных источников, включающего 105 наименований. Общий объем работы составляет 107 страниц текста.

1. Акишев, И.Р. Разработка и анализ параллельных поисковых структур данных, нечувствительных к размеру кеша / И.Р. Акишев. -Бакалаврская работа. Кафедра компьютерных технологий. -СПбГУИТМО, 2008. Режим доступа: http://is.ifmo.ru/present/

2. Norrish, M. С formalized in HOL / M. Norrish. PhD thesis. Univ. of Cambridge. Computer Lab., 1998. - 57 p.

3. Vafeiadis V. Modular fine-grained concurrency verification. PhD thesis. -Univ. of Cambridge. Computer Lab., 2008. 148 p.Монографии

4. Алешина, H.A. Логика и компьютер. Моделирование рассуждений и проверка правильности программ / H.A. Алешина, A.M. Анисов, П.И. Быстрое. М.: Наука, 1990. - 240 с.

5. Кларк, Э.М. Верификация моделей программ: Model Checking / Э.М. Кларк, О. Грамберг, Д. Пелед / ред. Р. Смелянский. М.: МЦНМО, 2002.-416 с.

6. Бройдо В.Л., Ильина О.П, Архитектура ЭВМ / В.Л. Бройдо, О.П. Ильина. М.: Научный мир, 2005. - 272 с.

7. Левин, М.П. Параллельное программирование с использованием ОрепМР / М.П. Левин. М.: Интернет-Университет Информационных Технологий. БИНОМ. Лаборатория знаний, 2008. - 118 с. - Лит.: С. 113-118.

8. Бурдонов, И.Б. Обзор подходов к верификации распределенных систем / И.Б. Бурдонов, A.C. Косачев, В.Н. Пономаренко, В.З. Шнитман. М.: ИСП РАН, 2003. - 52 с. - Ли.: С. 49-52.

9. Гуц, А.К. Математическая логика и теория алгоритмов: Учебное пособие. Омск: Наследие, 2003. - 108 с. - Лит.: С. 105-108.Ю.Дейкстра, Э. Дисциплина программирования / Э. Дейкстра. М.: «Мир», 1978. - 275 с.

10. Игошин, В.И. Математическая логика и теория алгоритмов: учебное пособие / В.И. Игошин. М.: «Академия», 2008. - 448 с. - Лит.: С. 435442.

11. Серебряков, В.А. Теория и реализация языков программирования / В.А. Серебряков, М.П. Галочкин, Д.Р. Гончар, М.Г. Фуругян. М.: МЗ-Пресс, 2003. - 296 с.

12. Хоар, Ч. Взаимодействующие последовательные процессы / Ч. Хоар. -М.: Мир, 1989.-264 с. -Избр. лит.: С. 254.

13. Intel Architecture Software Developer's Manual. Volume 1. - 244 p. -Режим доступа: http://www.intel.com/Assets/PDF/manual/245317.pdf

14. Fraser, К. Practical lock-freedom / K. Fraser . — University of Cambridge, 2004.-116 p.

15. Herlihy, M. The Art of Multiprocessor Programming / M. Herlihy, N. Shavit. Elsevier: Morgan Kaufmann, 2008. - 508 p.

16. Reed, J.N. Deductive Reasoning versus Model Checking: Two Formal Approaches for System Development // J.N. Reed, J.E. Sinclair, F. Guigard. Oxford Brookes, 1999.

17. Использование Thread Analyzer для поиска конфликтов доступа к данным. Режим доступа:http://ru.sun.com/developers/sunstudio/articles/tha using ru. html

18. Калугин, А. Верификатор программ на языке Си LINT / А. Калугин. -Режим доступа: http://www.viva64.com/go.php?url=224

19. Карпов, А. Что такое "Parallel Lint"? / А. Карпов. Режим доступа: http://software.intel.com/ru-ru/articles/parallel-lint/

20. Карпов, А. Тестирование параллельных программ / А. Карпов. -Режим доступа: http://www.softwaretesting.ru/library/testing/functionaltesting/5 81 -parallelprogramtesting

21. Прокопенко A.C. Дедуктивный метод анализа логических гонок с использованием сепарационной логики/Прокопенко A.C., Тормасов А.Г. // Труды МФТИ. — М.,2010. Т.2. № 3. - С. 175-184.

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

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

24. Кулямин, В. В. Интеграция методов верификации программных систем. Режим доступа: http://panda.ispras.ru/~kuliamin/docs/IntVer-2009-ru.pdf

25. Патил, Рахул В. и Джордж, Б. Средства и приемы для выявления проблем параллельного выполнения / Рахул В. Патил, и Б. Джордж //Журнал MSDN Magazine. 2008. - Июнь. - Режим доступа: http://msdn.microsoñ.com/ru-ru/magazine/cc546569.aspx

26. Adve S. V. Shared memory consistency models: A tutorial / S. V. Adve, K. Gharachorloo // Computer. 1996. - Vol. 29. - № 12. - 32 p. - Режим доступа: http://www.hpl.hp.com/techreports/Compaq-DEC/WRL-95-7.pdf

27. Arora, N.S. Thread scheduling for multiprogrammed multiprocessors /N.S. Arora, R.D. Blumofe, and C.G. Plaxton // Proc. of the Tenth Annual ACM Symposium on Parallel Algorithms and Architectures. ACM Press, 1998. -P. 119-129.

28. Balasundaram, V. Compile -time detection of race conditions in a parallel program / V. Balasundaram , K. Kennedy // Proceedings of the 3rd International conference on Supercomputing. Crete (Greece), 1989. - P. 175-185.

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

30. Barnes, G. A method for implementing lock -free shareddata structures / G. Barnes Proceedings of the fifth annual ACM symposium on Parallel algorithms and architectures. Velen (Germany), 1993. - P. 261-270.

31. Berdine, J. Symbolic execution with separation logic / J. Berdine, C. Calcagno, and Peter W. O'Hearn // APLAS. Vol. 3780 of Lecture Notes in Computer Science. 2005. - Springer. - P. 52-68.

32. Bach, M. The design of the UNIX operating system / M. Bach // Software. Series. Sec 5. 12.-Prentice-Hall, 1986.-P. 111-119.

33. Bodden, E. Racer: effective race detection using AspectJ / E. Bodden, K. Havelund. ISSTA, 2008. - Режим доступа: http://www.havelund.com/Publications/issta2008.pdf

34. Bornat, R. Permission accounting in separation logic / R. Bornat, C. Calcagno, P. W. O'Hearn, and M. J. Parkinson // 32nd ACM Symposium onPrinciples of Programming Languages (POPL 2005). ACM. 2005. - P. 259-270.

35. Bornat, R. Variables as resource in separation logic / R. Bornat, C. Calcagno, and H. Yang // Electronic Notes in Theoretical Computer Science. 2006. - 155. - P. 247-276.

36. Brookes, St. D. A semantics for concurrent separation logic // St. D. Brookes // 15th International Conference on Concurrency Theory (CONCUR). Vol. 3170 of Lecture Notes in Computer Science r. Springe. -2004.-P. 16-34.

37. Brookes, St. D. Variables as resource for shared-memory programs: Semantics and soundness / St. D. Brookes // Electronic Notes in Theoretical Computer Science. 2006. - 158. - P. 123-150.

38. Calcagno, C. Modular safety checking for fine-grained concurrency / C. Calcagno, M. Parkinson, and V. Vafeiadis // 14th International Static Analysis Symposium (SAS 2007). Vol. 4634 of Lecture Notes in Computer Science. 2007. - August. - P. 233-238.

39. Chase, D.R. Analysis of pointers and structures / D.R. Chase, M. Wegman, and F. K. Zadeck // Proceedings of the SIGPLAN '90 Conference on Programming Language Design and Implementation. June 1990. - P. 296310.

40. Cliff, B. J. Wanted: a compositional approach to concurrency / B,J. Cliff // Programming Methodology. Springer-Verlag. - 2003. - P. 5-15.

41. Cliff, B.J. Specification and design of (parallel) programs / B.J. Cliff // IFIP Congress. 1983. - P. 321-332.

42. Coleman, J. W. A structural proof of the soundness of rely/guarantee rules / J.W. Coleman and B.J. Cliff // Technical Report CS-TR-987. School of Computing Science. Newcastle University. - 2006. - October. - P. 807841.

43. Deutsch, A. Interprocedural May-Alias Analysis for Pointers : Beyond k-limiting / A. Deutsch // Proc. Programming Language Designand Implementation. ACM Press. 1994. - Vol. 29. - № 6. - P. 230-241.

44. Dodds, M. Deny-guarantee reasoning / M. Dodds, X. Feng, M. Parkinson, and V. Vafeiadis // Proc. ESOP. 2009. - P. 363-377.

45. Emanuelsson, P. A Comparative Study of Industrial Static Analysis Tools / P. Emanuelsson, U. Nilsson. Elsevier Science Publishers В. V. Amsterdam, The Netherlands, The Netherlands, 2008. Vol. 217. - P. 5-21.

46. Farzan, A. Algorithms for Atomicity / A. Farzan, P. Madhusudan. 2007.- Режим доступа:http ://scholar. google. com/scholar?q=25 .%09Farzan,+A.+Algorithms+forhA tomicity&hl=en&assdt=0&asvis=l&oi=scholart

47. Feng, X. Local rely-guarantee reasoning / X. Feng // ACM Symposium on Principles of Programming Languages. — 2009. P. 315-327.

48. Feng, X. On the relationship between concurrent separation logic and assume-guarantee reasoning / X. Feng, F. Rodrigo, S. Zhong // Proc. 16th European Symp. on Prog. (ESOP'07). Lecture Notes in Computer Science.- 2007.-Vol. 4421.-P. 173-188.

49. Flanagan, С. Types for atomicity / C. Flanagan and Sh. Qadeer // ACM Workshop on Types in Language Design and Implementation. ACM. -2003. January. - P. 1-12.

50. Gao, H. A general lock-free algorithm using compare-and-swap / H. Gao , W.H. Hesselink // Information and Computation, February, 2007. P. 225241.

51. Gotsman, A. Proving that non-blocking algorithms don't block / A. Gotsman, B. Cook, M. Parkinson, V. Vafeiadis // Proc. 36th ACM. Symp. on Principles of Prog. Lang. (POPL'09). ACM Press. - 2009. - P. 16-28.

52. Jones, C. Specification and design of (parallel) programs / C. Jones // Proceedings ofIFIP'83. -North-Holland, 1983. -P. 321-332.

53. Jones, C. Wanted: a compositional approach.to concurrency / C. Jones // In Programming Methodology, pages 5-15. Springer-Verlag, 2003.

54. Herlihy, M. Impossibility and Universality Results for Wait / M. Herlihy // . Free Synchronization, Proceedings of the seventh annual ACM Symposiumon Principles of distributed computing, 1988. — P. 276-290.

55. Herlihy, M.P. Linearizability: a correctness condition for concurrent objects // M.P. Herlihy and. J.M. Wing // ACM Transactions onProgramming Languages and Systems (TOPLAS). 1990. - Vol. 12. - № 3.-P. 463-492.

56. Herlihy, M.P. Wait-free synchronization / M.P. Herlihy // ACM Transactions on Programming Languages and Systems (TOPLAS). 1991. -13(1).-P. 124-149.

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

58. Herlihy, M.P. Obstruction-free synchronization: Double-ended queues as an example / M.P. Herlihy, V. Luchangco, and M. Moir // 23rd IEEE International Conference on Distributed Computing Systems. — 2003. -May.-P. 522-529.

59. Herlihy, M. A lock-free concurrent skiplist with wait-free search / M. Herlihy, Y. Lev, N. Shavit. Unpublished Manuscript. Sun Microsystems Laboratories. Burlington (Massachusetts), 2007.

60. Hoare, C.A.R. An axiomatic basis for computer programming / C.A.R. Hoare // Communications ACM. 1969. - Vol. 12. - № 1. - P. 576-580.

61. Hussak, W. Specifyning Strict Serializability of Iterated Transactions in Propositional Temporal Logic / W. Hussak // International Journal of Computer Science. 2007. - Vol. 2. - № 2. - Режим доступа: http ://www.ij csi.org/

62. Marginean, P. Lock-Free Queues / P. Marginean // Dr. Dobb's Journal. -July 2008. P. 43- 47. - Режим доступа:http://www.nxtbook.com/nxtbooks/cmp/ddj0708/index.php?startid=43#/46

63. McKenney, P.E. Selecting locking primitives for parallel programming / P.E. McKenney // Communications of the ACM. ACMPress. 1996. - Vol. 39. - № 10. - P. 75-82. - Режим доступа: http://portal.acrn.org/citation.cfm?id=236156.236174

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

65. Michael, M.M. Simple, fast, and practical nonblocking and blocking concurrent queue algorithms / M.M. Michael, M.L. Scott // Proc. of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing. ACM Press, 1996. - P. 267-275.

66. Mostefaoui, A. The combined power of conditions and failure detectors to solve asynchronous set agreement / A. Mostefaoui, S. Rajsbaum, M. Raynal // Proceedings of Symposium on Principles of Distributed Computing. ACM. Germany, 2005. - P. 179-188.

67. Li, M. How to share concurrent wait-free variables / M. Li, J. Tromp, and P.M.B. Vitanyi // Journal of the ACM. 1996. -Vol. 43. - № 4. - P. 723746.

68. Luchangco, V. Nonblocking k-compare-single-swap / V. Luchangco, M. Moir, N. Shavit // Proceedings of the fifteenth annual ACM symposium on Parallel algorithms and architectures. San Diego, 2003. - P. 314-323.

69. Naik, M. Effective Static Race Detection for Java / M. Naik, A. Aiken, J. Whaley // ACM SIGPLAN Notices. Proceedings of the 2006. PLDI Conference. 2006. - Vol. 41. - № 6. - P. 308-319.

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

71. Purcell, С. Non-blocking hashtables with open addressing / C. Purcell, T. Harris. — University of Cambridge, 2005. Режим доступа: http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-639.html

72. Reynolds, С. Separation logic: A logic for shared mutable data structures / C. Reynolds // Proc. 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02). IEEE Computer Society, 2002. - P. 55-74.

73. Michiel Ronsse, Koen De Bosschere, Non-Intrusive on-the-Fly Data Race Detection Using Execution Replay, Automated And Algorithmic Debugging: Proceedings of the IVIW on AD. Vol. I. Germany, 2000.

74. Qadeer, S. KISS: keep it simple and sequential / S. Qadeer, D. Wu. PLDI, 2004. - Режим доступа: http://faculty.ist.psu.edu/wu/papers/kiss.pdf

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

76. Scott, M.L. Non-blocking timeout in scalable queue-based spin locks / M.L. Scott // PODC Гf02: Proc. of the Twenty-first Annual Symposium on Principles of Distributed Computing. ACM Press. N.-Y., 2002. - P. 3140.

77. Shavit, N., Touitou, D. Software transactional memory / N. Shavit, D. Touitou // Proceedings of the 14th ACM Symposium on Principles of Distributed Computing. ACM. NY, 1995. - P. 204-213.

78. Steensgaard, B. Points-to Analysis in Almost Linear Time / B. Steensgaard // ACM POPL. 1996. - P. 1-10. - Режим доступа: http://www.cs.cornell.edu/courses/cs71 l/2005fa/papers/steensgaard-popl96.pdf