Статический анализ проблем синхронизации параллельных алгоритмов в вычислительных системах с общей памятью тема диссертации и автореферата по ВАК РФ 05.13.18, кандидат физико-математических наук Бабичев, Сергей Леонидович

• Бабичев, Сергей Леонидович
• кандидат физико-математических наук
• 2012

Оглавление диссертации кандидат физико-математических наук Бабичев, Сергей Леонидович

Содержание

Стр.

Список сокращений

ВВЕДЕНИЕ

Глава 1. ОБЗОР ОСНОВНЫХ МЕТОДОВ И МОДЕЛЕЙ

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

1.2. Обзор работ по теме

1.3. Сети Петри как инструмент моделирования дискретных систем

1.4. Терминология сетей Петри

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

1.5.1. Последовательное исполнение

1.5.2. Синхронизация

1.5.3. Слияние

1.5.4. Параллельное исполнение

1.5.5. Моделирование конфликтов

1.6. Классификация сетей Петри

1.6.1. Классификация активностей

1.6.2. Сифоны и ловушки

1.6.3. Применимость сифонов и ловушек в задачах определения тупиков

1.7. Резюме

Глава 2. МЕТОДЫ АНАЛИЗА СЕТЕЙ ПЕТРИ

2.1. Методы анализа активности сетей Петри

2.2. Метод дерева достижимости

2.2.1. Алгоритм построения дерева достижимости

2.3. Метод сифонов и ловушек

2.3.1. Теорема о минимальных сифонах

2.3.2. Теорема о задаче квадратичного программирования

2.3.3. Метод математического программирования

2.3.4. Метод минимальных сифонов

2.4. Сравнение методов

2.5. Резюме

Глава 3. СИНТЕЗ СОВОКУПНОЙ МОДЕЛИ

3.1. Примитивы синхронизации

3.1.1. Соглашения о терминологии

3.1.2. Примитив типа Mutex

3.1.3. Примитив типа Event

3.1.4. Действие типа Thread

3.1.5. Точка исполнения Action

3.2. Синтез совокупной сети Петри

3.2.1. Формализованный язык описания модели

3.2.2. Лексический анализ

3.2.3. Грамматический анализ ФОЯМ

3.2.4. Структуры данных грамматического анализа

3.2.5. Построение синтаксического дерева

3.2.6. Оптимизация

3.2.7. Исследование свойств совокупной сети Петри

3.3. Примеры использования

3.3.1. Классический пример тупика

3.3.2. Проблема синхронизации Apache deadlock bug #42031

3.3.3. Проблема обедающих философов

3.4. Резюме

Глава 4. ПРАКТИЧЕСКОЕ ПРИМЕНЕНИЕ МЕТОДОВ АНАЛИЗА

4.1. Практические задачи системного программирования, требующие решения

4.2. Пул вычислительных потоков (ПВП)

4.2.1. Требования, накладываемые на реализацию ПВП

4.2.2. Организация ПВП и методы работы с пулом

4.2.3. Оптимизация использования ПОВП

4.2.4. Операции ПОВП

4.2.5. Использование ПОВП для обработки запросов ввода-вывода

4.3. Апробация модели - драйвер-фильтр ввода/вывода

4.4. Апробация модели - решение задачи целочисленного математического программирования

4.5. Резюме

ЗАКЛЮЧЕНИЕ

СПИСОК ИСПОЛЬЗОВАННЫХ МАТЕРИАЛОВ

Список сокращений

ЗВН — защищённые виртуальные носители

МЗС — модифицированная защищённая среда

ПОВП — пул облегчённых вычислительных потоков

ПВП — пул вычислительных потоков

ФЯОМ — формализованный язык описания модели

ЯВУ — язык высокого уровня

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

ВВЕДЕНИЕ

Актуальность

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

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

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

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

В работе:

1. разработана новая конкретизация сети Петри для модели примитива синхронизации Event;

2. доказана теорема о маркировках, содержащих специальное значение счётчика маркеров

3. доказана теорема о соответствии предложенной сети Петри семантике примитива синхронизации Event;

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

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

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

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

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

Апробация работы.

Научные и практические результаты диссертации доложены, обсуждены и получили одобрение специалистов на:

• 48,49,50,51,52,53 научных конференциях МФТИ (Москва, 2007-2011);

• научных семинарах кафедры информатики МФТИ (Москва, 2007-2011);

• научных семинарах кафедры математических и информационных технологий МФТИ (Москва, 2007-2011);

• семинаре группы сопровождения переносной вычислительной техники ОАО Альфа-Банк (Москва, 2008)

• семинаре отдела безопасности ОАО БИНБАНК (Москва, 2007)

• научно-практическом семинаре Департамента защиты информации ОАО "ТНК-ВР Менеджмент"(Москва, 2010)

• семинаре административного отдела ООО "Прогресстех" (Москва, 2011)

• семинаре отдела защиты информации "ОАО ЛУКОЙЛ "(Москва, 2009)

• научно-технических семинарах Департамента системной интеграции ОАО "Форт-Диалог"(Набережные Челны, 2009-2011)

• семинаре отдела ЭВТ ООО "Татнефть"(Нурлат, 2008) и других.

По теме диссертации опубликовано 9 печатных работ, из них в реферируемых журналах — 2.

Объем и структура диссертации.

Диссертация изложена на 106-х страницах машинописного текста и состоит из введения, обзора литературы, основных методов и моделей исследования, трёх глав собственных исследований, заключения, библиографического указателя. Работа иллюстрирована 20-ю рисунками, 3-мя таблицами. Библиография включает 19 отечественных и 44 иностранных источников. Весь материал, представленный в диссертации, получен, обработан и проанализирован автором лично.

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

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

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

Заключение диссертации по теме «Математическое моделирование, численные методы и комплексы программ», Бабичев, Сергей Леонидович

вывода

-О ф О. ш т о ее га ос X со л «С ф о. ф

3"

О ж

05 а" ж X и X

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

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

На рисунках 4.4 и 4.5 показано распределение частоты размера запросов ввода/вывода для сценариев "Рабочая станция"и "Сервер"соответственно. Информация о распределении была получена с помощью драйвера виртуального носителя, входящего в состав оптимизируемой системы и представляет собой статистику, собранную за месяц работы на нескольких рабочих станциях и серверах. Распределение частот по длинам пакетов существенно разное, однако в обоих режимах основную группу составляют запросы размером, большим или равным 32 килобайт.

Задача обработки данного входного потока представляет из себя типичную задачу массового обслуживания.

Оптимизированная обработка запросов ввода-вывода л

С£ ф о. ш о ix го (Я

X ей

Прёофм^х. швание л с[ ш о. ф о « го, к X и зь

Рис. 4.3. Оптимизированная схема преобразования операций ввода-вывода

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

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

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

• Поток не имеет последствий, так как число событий на интервале (£, £ + х) не зависит от числа событий на непересекающемся с ним интервале (¿1,^1 + х)

• Поток стационарен, так как вероятность появления события на интервале (£, £ + ж) не зависит от времени t а зависит только от х

Размер запроса 512 <2048 <4096

Частота запроса 0,002 0,013 0.069 CL310 0,361 0,403 1 ! :-г:

512 <1024 <2048 S4096 <8192 <16384 <32768 <131072

Рис. 4.4. Распределения размеров запросов ввода/вывода в сценарии Рабочая станция по частоте

Следовательно, исходный поток является потоком Пуассона.

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

Обозначим как tin - момент времени, в который запрос поступил во входную очередь обработчика, - время, затрачиваемое на инициацию обработки, V - скорость обработки, tfin - время, затрачиваемое на завершение обработки, L - длину обрабатываемого запроса. Тогда tin tinit где tb ~ момент времени, в который запрос поступил на обработку. te = tb у где te - момент времени, в который запрос покинул обработку

Размер 512 <1024 <2048 <4096 <8192 <16384 <32768 <13107 запроса

Частота 0.000 о,соо 0,002 0,057 0 ;?!- 0Л27 Ц i о CJ L000 запроса 1,000 ; :. 0,800 -, -- . — о.боо f~ , ---- гШ.:1 о,4оо ; 0,200 • --------- -illi !.

0,000 — ------- .

512 <1024 <2048 <4096 <8191 <16384 £-32763 < ::.Ю72

Рис. 4.5. Распределения размеров запросов ввода/вывода в сценарии Сервер по частоте tout — te + tfin где tout ~ момент времени, в который запрос поступил в выходную очередь. Общее время прохождения запроса ttotal — tinit у tjin

Алгоритм aes-i:s ÀES-256 gost :si-p-se

Сксрсеть 35 МБ с 29 МЪ с :G МБ/С:

Рис. 4.6. Приблизительная приведённая скорость криптографического преобразования на 1ГГц одного ядра Intel Соге2

Для различных криптографических алгоритмов была измерена скорость криптографического преобразования и использованием ПВП с тремя дополнительными вычислительными потоками на вычислительной системе, состоящей из четырёхядерного процессора Intel Í5-2500K, работающего на тактовой частоте 4000 мегагерц с отключенным механизмом TurboBoost.

Измерения показали, что tinu -С у и t¡in <С следовательно, ttotai — у и время прохождения запроса постоянной длины обратно пропорционально скорости обработки.

4 т.

3.5 -'•

3 .

2,5

2

1,5 4

1 ■)

0, 5 о 4

12 3 4

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

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

4.4. Апробация модели - решение задачи целочисленного математического программирования

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

12 3 4

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

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

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

Созданная модель модифицированного пула облегчённых вычислительных потоков была записана на ФЯОМ следующим образом: shared mutex DataLockMutexO; shared mutex DataLockMutexl; shared mutex DataLockMutex2; shared mutex DataLockMutex3; shared event DataReadyEventO; shared event DataReadyEventl; shared event DataReadyEvent2; shared event DataReadyEvent3; shared event ResultReadyEventO; shared event ResultReadyEventl; shared event ResultReadyEvent2; shared event ResultReadyEvent3; shared mutex TableMutex; thread mainThread { forever {

DataLockMutexO.wait; OSetDataO;

DataReadyEventO. set; DataLockMutexl.wait; OSetDatal;

DataReadyEventl.set; DataLockMutex2.wait; @SetData2;

DataReadyEvent2.set; DataLockMutex3.wait; @SetData3;

DataReadyEvent3.set; ©work; Исполнение работы главного потока Ожидание завершения исполнения ResultReadyEventO.wait; DataLockMutexO.release; ResultReadyEventO.reset; ResultReadyEventl.wait; DataLockMutexl.release; ResultReadyEvent1.reset; ResultReadyEvent2.wait; DataLockMutex2.release; ResultReadyEvent2.reset;

ResultReadyEvent3.wait; DataLockMutex3.release; ResultReadyEvent3.reset; TableMutex.wait; @tableconsolidation; TableMutex.release; Потоки пула thread PoolThreadO { forever {

DataReadyEventO.wait; ©workO;

TableMutex.wait; @tableaddition; TableMutex.release; DataReadyEventO.reset; ResultReadyEvent0.set; thread PoolThreadl { forever {

DataReadyEventl.wait; ©workl;

TableMutex.wait; @tableaddition; TableMutex.release; DataReadyEvent1.reset; ResultReadyEvent1.set; thread PoolThread2 { forever {

DataReadyEvent2.wait; @work2;

TableMutex.wait; @tableaddition; TableMutex.release; DataReadyEvent2.reset; ResultReadyEvent2.set; thread PoolThread3 { forever {

DataReadyEvent3.wait; @work3;

TableMutex.wait; @tableaddition; TableMutex.release; DataReadyEvent3.reset; ResultReadyEvent3.set;

Данная модель была транслирована в сеть Петри. После прохода оптимизации модель содержала 72 позиции и 59 переходов. Модель показала отсутствие тупиков и реализована на ЯВУ. В качестве примитивов синхронизации mutex в реализации для эффективности выступали примитивы синхронизации CRITICAL SECTION.

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

Позиций / переходов 32/26 38/31 47/38

MIP, 1 ядро 36.1 6719 >36000

MIP, 2 ядра 19.8с 3821 >36000

MIP, 3 ядра 14.4с 2885 >36000

MIP, 4 ядра 11.0с 2101 >36000

Cordone, 1 ядро 4.31 47.98 1058

Tree, 1 ядро <0.01 0.01 0.03

ЗАКЛЮЧЕНИЕ

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

В работе:

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

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

3. Разработан формализованный язык описания модели (ФЯОМ), разработаны алгоритмы для синтеза совокупных сетей Петри по описанию модели параллельных вычислительных потоков на формализованном языке. Для хорошо известных примеров построены модели на формализованном языке описания модели. Результаты верификации данных моделей совпали с общепринятыми.

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

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

При сравнении методов анализа сетей Петри на наличие тупиков можно сделать следующие выводы:

• методом дерева состояний успешно решались задачи, синтезированные ФЯОМ, с числом позиций 98 и числом переходов 80;

• методом минимальных сифонов успешно решались задачи размером до 66 позиций и 54 переходов;

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

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

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

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

9. Модель пула облегчённых вычислительных потоков была признана подходящей для решения ряда задач системного программирования, в том числе для эффективной реализации криптографической обработки информации. Использованные алгоритмы и программы реализованы в составе программных продуктов "StrongDisk Pro "StrongDisk CorporateMH

StrongDisk Server которые широко эксплуатируется с 2006 года и показали высокую эффективность и надёжность.

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

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

Список литературы диссертационного исследования кандидат физико-математических наук Бабичев, Сергей Леонидович, 2012 год

Список литературы

1. Ахо А., Ульман Док. Теория синтаксического анализа, перевода и компиляции, -М.:Мир, 1978, т. 1,2.

2. Бабичев С. Л., Коньков А. ККоньков К. А. Дополнительная защита ресурсов операционной системы методом криптографической защиты данных // Моделирование процессов обработки информации:Сборник научных трудов МФТИ./ - М., 2007, -С. 251-259

3. Семененко В. Л., Бабичев С. Л., Бобьяков А. С., Коньков А. К., Коньков К. А., Телицын М. А. Защита корпоративной информации от внутренних угроз на основе метода доверенной загрузки системы// Современные проблемы фундаментальных и прикладных наук. Современные проблемы фундаментальных и прикладных наук: Труды 50-й научной конференции МФТИ./ -М,-Долгопрудный, 2007, -С. 174-175

4. Бабичев С. Л., Бобьяков А. С., Коньков А. Кv Коньков К. А. "Математическая модель защищенной компьютерной системы под управлением Windows// Современные проблемы фундаментальных и прикладных наук: Труды 51-й научной конференции МФТИ./ -М.-Долгопрудный, 2008, Т 2. -С. 56-57.,

5. Бабичев С. Л., Бобьяков А. С., Коньков А. К., Коньков К. А. Эффективное использование ресурсов вычислительных систем при решении задач информационной безопасности// Современные проблемы фундаментальных и прикладных наук. Часть VII Управление и прикладная математика: Труды 52-й научной конференции МФТИ./ -М.Долгопрудный, 2009, Т 3. -С. 7-8.

6. Бабичев С. Л., Коньков А. К., Коньков К. А. Об оптимальном использовании ресурсов вычислительной системы для реализации модифицированной защищенной среды// Современные проблемы фундаментальных и прикладных наук. Часть VII Управление и прикладная мате-

матика: Труды 53-й научной конференции МФТИ/ -М.-Долгопрудный, 2010

7. Бабичев С. Л., Коньков А. К., Коньков К. А. Автоматизированный анализ проблем синхронизации параллельных алгоритмов в вычислительных системах с общей памятью // Современные проблемы фундаментальных и прикладных наук. Современные проблемы фундаментальных и прикладных наук: Труды 54-й научной конференции МФТИ/ - М,-Долгопрудный, 2011 -С.48-49

8. Бабичев С. Л., Коньков А. К., Коньков К. А. Использование пула вычислительных потоков со статическим планированием для оптимизации подсистемы защищённых виртуальных носителей модифицированной защищённой среды// Труды МФТИ/ 2012, -М.-Долгопрудный

9. Бабичев С. Л., Коньков А. К., Коньков К. А. Применение сетей Петри для диагностирования проблем синхронизации в вычислительных системах с общей памятью// Труды МФТИ/ 2012, -М,-Долгопрудный

10. Безбедова Л. Л., Ключко В. И. Теория вычислительных процессов, Краснодар, издательство КубГУ, 2004 47с.

11. Васильев В. В Кузьмук В. В. Сети Петри, параллельные алгоритмы и модели мультипроцессорных систем- Киев, Наукова думка, 1990

12. Грис Д. Конструирование компиляторов для цифровых вычислительных машин. -М.:Мир, 1975

13. Карманов В. Г. Математическое программирование, -М., 2008, ФИЗ-МАТЛИТ

14. Карпов В. Е., Коньков К. А. Основы операционных систем. Курс лекций. Учебное пособие. / Под редакцией В. П. Иванникова. -М.: ИНТУ-ИТ. РУ Интернет-Университет информационных технологий, 2004, -С. 1-632

15. Коньков К. А. Устройство и функционирование ОС Windows, практикум к курсу Операционные системы: учебное пособие/ К. А. Коньков. -М.: Интернет-Университет Информационных технологий; БИНОМ. Лаборатория знаний, 2008. - 207 с.

16. Котов В. Е. Сети Петри// Главная редакция физико-математической литературы./ -М.: Наука. - 1984.

17. Питерсон Д. Теория сетей Петри и моделирование систем, — -М. Мир, 1984. - 264 с.

18. Рихтер Дж. Windows для профессионалов: создание эффективных Win32-nptmo>KeHHft с учётом специфики 64-разрядной версии Windows/Пер. с англ. - 4-е издание - СПб: Питер; М.: Издателько-торговый дом Русская редакция,- 2004. - 749 с.

19. Серебряков В. А. Теория и реализация языков программирования. -М.:МЗ-Пресс, 1999

20. Banaszak Z. A. Krogh В. Н. Deadlock avoidance in flexible manufacturing systems with concurrency competing process flows// IEEE Trans. Robot. Automat./ 1990, Vol 6, -P. 724-734

21. Barkaoui K. Ben Abdallah I. An efficient avoidance control policy in FMS using structural analysis of Petri nets// in Proc. IEEE SMC Conf./ San Antonio, TX, 1994

22. Barkaoui K. Couvreur J. M., Dutheillet C. On the liveness in extended non self-controlling nets// Advances in Petri Nets 1995/ New York: SpringerVerlag, 1995

23. Barkaoui, К Pradat-Peyre, J-F, On Liveness and Controlled Siphons in Petri Nets/Barkaoui, К Pradat-Peyre, J-F //Applications and theory of Petri nets 2005/ SpringerLink, 2005

24. Berthlot G. Checking properties of nets using transformation// Advances of Petri Nets 1985/ -New York: Springer-Verlag, 1995

25. Brams G. W. Reseaux de Petri: Theorie et Pratique -Masson, France, 1983

26. Campos, J, Chiola, G, Silva, M Ergodicity and throughput bounds of Petri nets with unique consistent firing vector// IEEE Trans Software Eng./ 1991, Vol 17, -P. 117-125

27. Chu F., Ian Xie I. Deadlock analysis of Petri nets using siphons and mathematical programming// IEEE Transactions of Robotics and Automation/ Vol. 13, No. 6. 1997 December.

28. Colom J. M., Silva M. Improving the linearly based characterization of P/T nets// Advances in Petri Nets 1990/ -New York: Springer-Verlag, 1991

29. Cordone, R, Ferrarini, L, Piroddi, L Characterization of Minimal and Basic siphons with Predicate Logic and Binary Programming Cordone, R, Ferrarini, L, Piroddi, L, //Proceedings of the 42nd IEEE Conference on Decision and Control/ pp 3754-3759, Maui, 2003

30. Cordone, R, Ferrarini, L, Piroddi, L Some Results on the Computation of Minimal Siphons in Petri Nets/ Cordone, R, Ferrarini, L, Piroddi, L, //Proceedings of the 42nd IEEE Conference on Decision and Control/ pp 3754-3759, Maui, 2003

31. Eilenberg S Automata Machines and Languages// vol. A/, Academic Press, New York, 1974.

32. Ezpeleta J. Colom J. M. Martinez J. A Petri net based deadlock prevention policy for flexible manufacturing systems// IEEE Trans. Robot. Automat./ 1995, vol. 11, -P. 173-184

33. Giua A. Petri nets as discrete event model for supervisory control // Renselaer Polytechnic Institute (Troy, New York). July 1992.

34. Govindarajan F., Suciu W. M., Zuberek P. Timed Petri NetModels of Multithreaded Multiprocessor Architectures//— IEEE Preceedings if the 7-th International Workshop on Petri Nets and Performance Models/, Saint Malo, 1997.-June.

35. Habermehl P., Meyer R., Wimmel H. The downward-closure of Petri net languages //ICALP. - 2010.

36. Iordache, M. V. Antsaklis, P. J Supervisory Control of Concurrent Systems:// A Petri Net Structural Approach/ Birhauser, 2006

37. Isard M., Birrell A. Automatic mutual exclusion// Proceedings of the 11th USENIX workshop on Hot topics in operating systems/ 2007, San Diego, CA, -P. 3:1-3:6

38. Jeng M. D. Dicesare F. Synthesis using resource control nets for modeling shared-resource systems// IEEE Trans. Robot. Automat./ 1995, vol 11, -P. 317-327

39. Karp R. Miller R. Parallel Program Schemata// IEEE Conference Record of the 1967 Eights Annual Simposium on Switching and Automata Theory/ New York: IEEE, 1967, -P. 55-61

40. Kavi, K. M., Bukhles P. B., Bhat N. U Isomorphism between Petri net and dataflow graphs // IEEE Transactions on Software Engineering/ Vol SE-13 No. 10. 1987. Nov.

41. Kavi, K. M., Moshtaghi A., Chen D.-J. Modeling multithreaded application using Petri nets // International Journal of Parallel Programming//, Vol. 30, Iss 5. 2002. October. -P. 1-23.

42. Krogh B. H., Beck .C .L Synthesis of place/transition nets for simulation and control of manufacturing systems// Proc. IFIP Symp. Large Scale Syst./ -Zurich, 1986

43. Lautenbach, K., Ridder, H. Liveness in bounded Petri nets which are covered by T-invariants// Advances in Petri Nets 1994/ -New York: Springer-Verlag, 1994

44. Lee K. H., Favral J. Hierarchical reduction method for analysis and decomposition of Petri nets// IEEE Trans. Syst., Man, and Cybern./ 1985, vol. SMC-15, pp 272-281

45. Lester B. P. Detection of control flow errors in parallel programs at compile time// International Journal of Distributed and parallel Systems (IJDPS)/ - Vol. 1, No. 2. - 2010. - November.

46. Minoux, M. Programmation Mathématique: Theorie and Algorithms -Dunod, Paris, France, 1983

47. Moshtaghi A. R. Modeling Multithreaded Programs Using Petri Nets// MS Thesis, Dept of ECE// The University of Alabama in Huntsville, Huntsville, AL 35899, May 2001

48. Murata, T. Petri nets: Properties, analysis and application // Proceedings of the IEEE,/ -Vol. 77, N 4. 1989. -P. 541-580

49. Padidar S Parallel Program Verification: A Brief Introduction //2010

50. Pommereau F. Petri Nets as Executable Specifications of High-Level Timed Parallel Systems// /2005, -P. 1-8

51. Rockafellar R. T. Convex Analysis, Princeton, NJ: Princeton University Press, 1972,

52. Silva M. Colom J. M. On the computation of structural synchronic invariants in P/T nets// Advances in Petri nets 1988/ -New York:Springer-Verlag, 1989

53. Suzuki I. Murata T. A method for stepwise refinement and abstraction of Petri Nets// J. Comput. Syst. Sci./ vol. 27, -P. 51-76, 1983

54. Takaoka T. A Systematic Approach to Parallel Verification // Department of Computer Science of Ibaraki University.// — 1995. — August.

55. Teruel E. Colom J. M. Silva M. Linear analysis of deadlock-dreeness of Petri net models// in Proc. 2nd European Cnttr. Conf./ -Groningen, The Netherlands, 1993

56. Vallejo F., Gregorio J. A., Gonzalez H. M., Drake J. M. Shared memory multiprocessor operating system with an extended Petri net model // IEEE transactions on parallel and distributing systems/, v5. N 7. 1994. -P. 749762.

57. Valette R. Analysis of Petri nets by stepwise refinements// J. Comput. Syst. Sci./ -1979. -Vol. 18. -P. 35-46

58. Viswanadham N., Narahari Y., Johnson T. L. Deadlock prevention and deadlock avoidance in flexible manufacturing system using Petri net models// IEEE Trans. Robot. Automat./ -1990 - Vol. 6, -P. 713-723

59. L-M Wang and X-L Xie Modular modeling using Petri nets// IEEE Trans. Robot. Automat./ -Vol 12, -P. 800-809, 1996

60. Wang, Y, Lafortune, S Kelly Discrete control for safe execution of IT automation workflows// ACM SIGOPS Operating Systems Review -EuroSys'07 Conference Proceedings/ Volume 41 Issue 3, June 2007

61. Wang, Y, Lafortune, S Kelly, T Kudlur, M Mahlke, S The Theory of Deadlock Avoidance via Discrete Control// ACM SIGPLAN Notices -POPL '09//' Volume 44 Issue 1, January 2009

62. Zhou M. C., DiCesare F. Parallel and sequential mutual exclusions for Petri net modeling of manufacturing systems with shared resources// IEEE Trans. Robot. Automat./ -Vol 7, -P. 515-527, 1991

63. Zhou M. C. Dicesare F. Desrochers A. A A Hubrid methodology for syntesis of Petri net models for manufacturing systems// IEEE Trans. Robot. Automat./ Vol. 8, -P. 350-361, 1992