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

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

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

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

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

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

В работе:

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 иностранных источников. Весь материал, представленный в диссертации, получен, обработан и проанализирован автором лично.

вывода.

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

3″ .

О ж.

05 а" ж X и X.

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

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

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

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

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

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

X ей.

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

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

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

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

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

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

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

Размер запроса 512 <2048 <4096 <16 384 <32 768 <13 107.

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

512 <1024 <2048 S4096 <8192 <16 384 <32 768 <131 072.

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

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

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

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

Размер 512 <1024 <2048 <4096 <8192 <16 384 <32 768 <13 107 запроса.

Частота 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 <16 384 ?-32 763 < :.Ю72.

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

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

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

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

Для различных криптографических алгоритмов была измерена скорость криптографического преобразования и использованием ПВП с тремя дополнительными вычислительными потоками на вычислительной системе, состоящей из четырёхядерного процессора Intel I5−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 DataLockMutexOshared mutex DataLockMutexlshared mutex DataLockMutex2- shared mutex DataLockMutex3- shared event DataReadyEventOshared event DataReadyEventlshared event DataReadyEvent2- shared event DataReadyEvent3- shared event ResultReadyEventOshared event ResultReadyEventlshared event ResultReadyEvent2- shared event ResultReadyEvent3- shared mutex TableMutexthread mainThread { forever {.

DataLockMutexO.waitOSetDataO-.

DataReadyEventO. setDataLockMutexl. waitOSetDatal-.

DataReadyEventl.setDataLockMutex2.wait- @SetData2-.

DataReadyEvent2.setDataLockMutex3.wait- @SetData3-.

DataReadyEvent3.set- (c)workИсполнение работы главного потока Ожидание завершения исполнения ResultReadyEventO.waitDataLockMutexO.releaseResultReadyEventO.resetResultReadyEventl.waitDataLockMutexl.releaseResultReadyEvent1.resetResultReadyEvent2.waitDataLockMutex2.releaseResultReadyEvent2.reset-.

ResultReadyEvent3.waitDataLockMutex3.releaseResultReadyEvent3.resetTableMutex.wait- @tableconsolidationTableMutex.releaseПотоки пула thread PoolThreadO { forever {.

DataReadyEventO.wait- (c)workO-.

TableMutex.wait- @tableadditionTableMutex.releaseDataReadyEventO.resetResultReadyEvent0.setthread PoolThreadl { forever {.

DataReadyEventl.wait- (c)workl-.

TableMutex.wait- @tableadditionTableMutex.releaseDataReadyEvent1.resetResultReadyEvent1.setthread PoolThread2 { forever {.

DataReadyEvent2.wait- @work2-.

TableMutex.wait- @tableadditionTableMutex.releaseDataReadyEvent2.resetResultReadyEvent2.setthread PoolThread3 { forever {.

DataReadyEvent3.wait- @work3-.

TableMutex.wait- @tableadditionTableMutex.releaseDataReadyEvent3.resetResultReadyEvent3.set-.

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

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

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

MIP, 1 ядро 36.1 6719 >36 000.

MIP, 2 ядра 19.8с 3821 >36 000.

MIP, 3 ядра 14.4с 2885 >36 000.

MIP, 4 ядра 11.0с 2101 >36 000.

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 и использованием данного примитива в критических секциях во всех вычислительных потоках. Данная модификация верифицирована и признана не имеющей тупиков..

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