Автоматическая верификация и оптимизация потоков работ
На правах рукописи
КАЛЕНКОВА АННА АЛЕКСЕЕВНА
АВТОМАТИЧЕСКАЯ ВЕРИФИКАЦИЯ И ОПТИМИЗАЦИЯ ПОТОКОВ РАБОТ
Специальность 05.13.11 – математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей
АВТОРЕФЕРАТ
диссертации на соискание ученой степени
кандидата физико-математических наук
Москва – 2011
Работа выполнена в Учреждении Российской академии наук Вычислительном центре им. А. А. Дородницына РАН
Научный руководитель:
доктор физ.-мат. наук
Серебряков Владимир Алексеевич
Официальные оппоненты:
доктор физ.-мат. наук
Флёров Юрий Арсениевич
кандидат физ.-мат. наук
Гайсарян Сергей Суренович
Ведущая организация:
Московский физико-технический институт (государственный университет)
Защита состоится «8» декабря 2011 года в 14 час. на заседании на диссертационного совета Д 002.017.02 при Учреждении Российской академии наук Вычислительном центре им. А. А. Дородницына РАН по адресу: Москва, улица Вавилова, дом 40, конференц-зал.
С диссертацией можно ознакомиться в библиотеке ВЦ РАН.
Автореферат разослан «7» ноября 2011 г.
| Ученый секретарь диссертационного совета Д 002.017.02 доктор физ.-мат. наук | Рязанов В.В. |
ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ
Актуальность темы
С распространением глобальной сети Интернет появилась возможность объединять географически распределенные вычислительные и человеческие ресурсы для координированного исполнения различных производственных процессов. Потоком работ принято считать формальное описание процедуры передачи данных и управления между участниками некоторого производственного процесса в соответствии с определенными правилами. Известны различные исполняемые языки описания потоков работ, такие как BPEL, XPDL, BPMN. Все они позволяют явно или неявно задавать поток управления с помощью таких маршрутизирующих элементов как «И-распараллеливание», «И-синхронизация», «ИЛИ-выбор», «ИЛИ-синхронизация», поэтому необходимы средства автоматической проверки сбалансированного использования этих элементов (верификации) при проектировании потоков работ. Кроме того, в ходе формализации производственного процесса может быть получен поток работ не оптимальный по времени выполнения. Так, например, поток работ может содержать конструкции, описывающие последовательное исполнение независящих по данным действий. Поэтому особый интерес представляет задача автоматического преобразования потока работ таким образом, что задания независящие по данным будут исполнены параллельно, при этом смысл самого потока работ будет сохранен.
Цель работы
Целью диссертационной работы является построение эффективных универсальных алгоритмов верификации и оптимизации (распараллеливания независящих по данным действий), подходящих для анализа и преобразования потоков работ, представленных на некотором исполняемом языке, в частности на BPEL. Для достижения этой цели были поставлены следующие задачи:
- Разработка единого промежуточного графового представления для моделирования потока управления и потока данных с целью анализа потоков работ, определенных с помощью различных языков описания потоков работ.
- Создание новых эффективных алгоритмов верификации и оптимизации потока работ, анализирующих произвольные структуры разработанного промежуточного графового представления.
- Для унифицированного анализа блочно-графовых языков описания потоков работ используется промежуточное блочно-графовое представление. Необходимы алгоритмы двустороннего отображения между созданным промежуточным графовым представлением и предложенным в литературе блочно-графовым базисным Формальным языком описания потоков работ.
- Разработка алгоритмов двустороннего отображения между Формальным языком описания потоков работ и языком BPEL для оценки практического применения алгоритмов анализа потоков работ.
Научная новизна
Научной новизной обладают следующие результаты диссертационной работы:
- Предложены новые эффективные алгоритмы верификации и оптимизации (распараллеливания независящих по данным действий) потоков работ;
- Разработано промежуточное графовое представление для моделирования потока управления и потока данных с целью анализа потоков работ, определенных с помощью различных языков описания потоков работ.
- Разработаны алгоритмы двустороннего отображения между созданным промежуточным графовым представлением и блочно-графовым представлением потока управления.
Практическая ценность
Разработанные промежуточное графовое представление потока управления и потока данных, алгоритмы работы с этим представлением, алгоритмы двустороннего отображения между этим представлением и блочно-графовым Формальным языком описания потоков работ, а также алгоритмы двустороннего отображения между конструкциями языка BPEL и Формальным языком описания потоков работ позволили создать Систему автоматического анализа и преобразования BPEL-процессов. Эта система была использована для анализа и преобразования производственных процессов Электронной библиотеки «Научное наследие России», формализованных с помощью языка BPEL. На основе доступных открытых кодов был создан прототип системы исполнения BPEL-процессов Электронной библиотеки «Научное наследие России». Предложенный алгоритм оптимизации BPEL-процессов имеет большое практическое значение, так как в настоящий момент нет методов и систем, позволяющих в полном объеме распараллеливать блочно-графовую структуру потока работ.
Апробация работы
Основные положения работы докладывались на восьмой всероссийской научной конференции «Электронные библиотеки: перспективные методы и технологии, электронные коллекции» (2006 г.), на 51-ой научной конференции «Современные проблемы фундаментальных и прикладных наук» (2008 г.), на четвертой международной конференции «Информационные технологии и системы: наука и практика» (2009 г.), на 52-ой научной конференции «Современные проблемы фундаментальных и прикладных наук» (2009 г.), на 17-ой всероссийской научно-методической конференции «Телематика» (2010 г.), на 13-ой всероссийской конференции «Распределенные информационно-вычислительные ресурсы» (2010 г.). Были опубликованы работы в журналах «Труды МФТИ» (2009 г.) и «Программирование» (2010 г.)
Публикации
По теме диссертации опубликовано 8 печатных работ.
Структура и объем работы
Работа состоит из введения, трех глав, заключения, списка литературы и трех приложений. Общий объем диссертации 164 страницы. Список литературы содержит 42 наименования.
СОДЕРЖАНИЕ РАБОТЫ
В Главе 1 рассказывается об основных понятиях предметной области (потоки работ, системы управления потоками работ), приводится описание основных известных языков представления потоков работ. Для анализа и преобразования потоков управления вводятся Размеченные графы анализа потоков работ.
Определение 1. Графом анализа потока работ (графом анализа) называется шестерка 
: 
- конечное множество вершин, 
- конечное множество заданий, 
- начальное задание, 
- конечное множество вершин выбора, 
- конечное множество вершин слияния, 
- поток управления (множество дуг). При этом выполнены условия: у начального задания нет входящих дуг, для каждой вершины кроме начального задания 
существует путь из 
в 
, только у заданий может не быть исходящих потоков управления, каждая вершина выбора имеет, по крайней мере, две исходящие дуги.
Граф анализа потока работ – это направленный граф, в котором вершины делятся на задания, выполняющие полезную работу, и координаторы выбора или слияния (Рис. 1). Граф анализа обладает не только статической, но и динамической составляющей – дуги графа могут содержать некоторое количество фишек или не содержать их вовсе. Фишки перемещаются по Графу анализа согласно определенным правилам.
Рис. 1. Элементы Графа анализа потока работ
Размеченный граф анализа – Граф анализа, дополненный некоторыми пометками. В частности, Размеченный граф анализа позволяет указать в качестве входных и выходных параметров глобальные переменные потока работ, дает возможность анализировать зависимости по данным.
Рассматриваются известные существующие графовые промежуточные представления потоков работ: Сети потоков работ и Графы потоков работ. Обосновывается выбор Размеченных графов анализа потоков работ в качестве промежуточного представления для анализа потока управления и потока данных. Для унифицированного анализа блочно-графовых языков описания потоков работ предлагается промежуточный язык – Формальный язык описания потоков работ, моделирующий поток управления и поток данных.
Определение 2. Поток работ, заданный с помощью Формального языка описания потоков работ, определяется шестеркой 
:
- Множество
- множество всех локальных генерируемых в процессе выполнения потока работ событий. - Множество действий
состоит из множества составных и простых действий, для которых определены формулы. - Начальное действие
. Действие, с которого начинается выполнение потока работ. - Множество переменных, определенных уровне экземпляра потока работ
. - Множество предикатов
. Предикаты являются функциями, принимающими значение булевского типа, они используются в логических выражениях условных конструкций потока работ. - Множество формул
, описывающих структуру действий потока работ. Каждая из формул этого множества определяет структуру простого или составного действия, идентификатор которого указан в ее левой части.
Действия потока работ могут быть простыми и составными. Составное действие строится из действий потока работ с использованием правил активации вложенных действий: параллельной и последовательной активации. Составное действие также может быть специальным составным действием: условным выбором или циклом. В формулах потока работ для простых действий указываются их имена, входные и выходные параметры (переменные потока работ). К простым действиям также относятся несколько специальных системных действий: генерация события, ожидание события с одновременным удалением информации о нем, пустое действие, не выполняющее никакой работы. Поток работ завершает свое выполнение, когда ни одно его действие не может быть активировано.
Приводятся алгоритм построения Размеченного графа анализа потока работ по Формальному описанию потока работ (Алгоритм 1) и обратный алгоритм получения Формального описания потока работ по Размеченному графу анализа (Алгоритм 2). Доказано утверждение об обратимости преобразований.
Утверждение 1. Пусть по Формальному описанию потока работ 
с помощью Алгоритма 1 построен Размеченный граф анализа потока работ 
. Тогда, если к Размеченному графу анализа потока работ 
применить Алгоритм 2, то он будет выполнен без ошибок, результатом его работы стает некоторое Формальное описание потока работ 
.
В Главе 2 для Размеченных графов анализа потоков работ представлены разработанные автором алгоритмы верификации и оптимизации потоков работ. Определены вычислительные сложности предлагаемых алгоритмов.
Алгоритмы верификации потоков работ позволяют находить вершины графа, моделирующего поток работ, в которых могут возникать структурные конфликты. Конфликт типа «тупик» возникает в том случае, если лишь некоторые из входящих дуг синхронизирующей вершины активированы, и синхронизирующая вершина будет бесконечно долго ожидать активации других входящих дуг. Конфликт типа «недостаток синхронизации» произойдет в ациклическом Размеченном графе анализа потока работ, если вершина слияния была активирована несколько раз вследствие активации различных входящих дуг. В работе представлен новый алгоритм верификации потоков работ - АБВ (алгоритм булевой верификации) для графов без ориентированных циклов (Алгоритм 3), в ходе работы которого каждой вершине выбора 
Размеченного графа анализа потока работ 
ставится в соответствие уникальный идентификатор 
, для каждой вершины 
и для каждой дуги 
определяются условие выполнения 
и условие активации 
соответственно, являющиеся булевыми функциями над множеством идентификаторов вершин выбора. Если условия активации входящих дуг синхронизирующей вершины не совпадают, возможен случай, когда будет активирована только часть входящих дуг, и возникнет конфликт типа «тупик». Условие выполнения вершины слияния вычисляется как дизъюнкция условий активации входящих дуг. Если условия активации входящих дуг являются попарно взаимоисключающими, то при выполнении потока работ может быть активировано не более одной входящей дуги вершины слияния, иначе возникнет конфликт типа «недостаток синхронизации». Пример работы Алгоритма 3 приведен на рисунке 2.
Рис. 2. Пример работы Алгоритма 3
Для задания 
условия активации входящих дуг: 
и 
различны, поэтому может возникнуть конфликт типа «тупик». Конфликт типа «недостаток синхронизации» может возникнуть в вершине слияния 
, условия активации входящих дуг которой: 
и 
.
Условия выполнения вершин и условия активации дуг представлены в виде дизъюнктивных нормальных форм (ДНФ) идентификаторов вершин выбора или их отрицаний. При этом в каждой конъюнкции первым указан идентификатор (или его отрицание) той вершины выбора, которая была раскрыта последней. Этот идентификатор или его отрицание называется ключевым фактором конъюнкции. Были доказаны теоремы, определяющие свойства представлений условий выполнения вершин и активации дуг.
Теорема 1. Пусть дан Размеченный граф анализа потока работ без ориентированных циклов 
, не содержащий структурных конфликтов. В ходе работы Алгоритма 3 было вычислено условие выполнения вершины выбора 
- 
, пусть оно было представлено в виде ДНФ - 
. Тогда для любой вершины графа 
представление условия ее выполнения либо содержит все дизъюнкты 
,…, 
, где 
- это 
или 
не более одного раза, либо не содержит ни один из этих дизъюнктов.
При слиянии потоков управления все дизъюнкты 
,…,
, 
,…,
заменяются на 
,…,
для сокращения представления условия выполнения вершины. После получения новых дизъюнктов должна быть проведена попытка повторного сокращения представления условия активации и так до тех пор, пока сокращение не сможет быть выполнено. Такие представления условий выполнения вершин и активации дуг называются сокращенными.
Теорема 2. Пусть дан Размеченный граф анализа потока работ без ориентированных циклов, не содержащий структурных конфликтов. В ходе работы Алгоритма 3 были вычислены условия выполнения вершин. Условия выполнения вершин совпадают тогда и только тогда, когда совпадают множества ключевых факторов дизъюнктов сокращенных представлений этих условий.
Теорема 3. Пусть дан Размеченный граф анализа потока работ без ориентированных циклов 
, не содержащий структурных конфликтов. В ходе работы Алгоритма 3 были вычислены условия активации входящих дуг 
,
вершины 
- 
, 
. Рассмотрим 
и 
- произвольные дизъюнкты представлений условий 
и 
соответственно. Пусть 
, 
и 
или 
, или 
такое, что 
. Тогда дизъюнкты 
и 
не являются взаимоисключающими, то есть 
.
Количество дизъюнктов при каждом новом слиянии может расти экспоненциально, поэтому вводятся ключевое и табличное представления условий выполнения вершин и активации дуг. Ключевое представление определяется как дизъюнкция ключевых факторов соответствующего сокращенного представления. Табличное представление – это таблица, каждая строка которой будет соответствовать некоторой вершине выбора графа, а точнее ее идентификатору. Табличное представление используется для определения конфликтов типа «недостаток синхронизации» и может быть получено по ключевому представлению. В работе доказано, что вычислительная сложность Алгоритма 3, работающего с ключевыми и табличными представлениями, составляет 
, где 
- количество дуг, 
- количество вершин выбора.
В работе представлен алгоритм булевой верификации потоков работ для графов с циклами (Алгоритм 4). В ходе работы Алгоритма 4 с графами, содержащими ориентированные циклы, выделяются вложенные циклы программы, каждый вложенный цикл программы проверяется на наличие конфликтов типа «мертвый цикл», «бесконечный цикл», «ветвящийся цикл» (рассматриваются вершины выхода из цикла и вершины инициирующие цикл), проводится верификация ациклического графа на каждом уровне вложенности. Сложность Алгоритма 4 совпадает с вычислительной сложностью Алгоритма 3. Обосновывается корректность и полнота Алгоритма булевой верификации для графов без ориентированных циклов (Алгоритм 3).
Предлагается алгоритм автоматической оптимизации Размеченных графов анализа потоков работ (Алгоритм 5), который преобразует граф на каждом уровне вложенности циклов программы, удаляя потоки управления, формирующие избыточные пути в графе, и сохраняя зависимости по данным и управлению (условия выполнения заданий и вершин выбора). Вычислительная сложность Алгоритма 5 
, где 
- количество вершин, 
- количество вершин выбора, а 
- количество переменных, используемых в качестве входных и выходных параметров вершин графа. Приводится модификация алгоритма оптимизации (Алгоритма 5), которая позволяет восстанавливать описание потока работ на Формальном языке по Размеченному графу анализа (с помощью Алгоритма 2), полученному в результате оптимизирующих преобразований. Дается обоснование того, что Алгоритм 5 не меняет функциональность (смысл) потока работ, если Размеченный граф анализа потоков работ удовлетворяет некоторым дополнительным условиям и не содержит структурных конфликтов.
В Главе 3 определяются правила прямого и обратного отображений между конструкциями языка BPEL и Формального языка описания потоков работ. Описывается Система автоматической верификации и оптимизации, реализующая предлагаемые алгоритмы анализа, преобразования и отображения, которая может быть использована для анализа и оптимизации потоков работ, формализованных с помощью языка BPEL. Излагаются основные принципы работы Электронной библиотеки «Научное Наследие России», обосновывается необходимость использования системы управления потоками работ для формализации и автоматизации управления процессами в электронной библиотеке, в качестве такой системы предлагается специально разработанная Система управления Электронной библиотекой «Научное наследие России», отвечающая за исполнение BPEL-описаний процессов. Рассматривается пример BPEL-процесса Электронной библиотеки «Научное наследие России», проводится его анализ и оптимизация в соответствии с предлагаемыми алгоритмами.
В Приложении 1 приведен псевдокод функций используемых при построении Формального описания потока работ по Размеченному графу анализа потока работ. В Приложении 2 и Приложении 3 представлен BPEL-процесс удаления книги в Электронной библиотеке «Научное наследие России» до и после оптимизирующих преобразований соответственно. В Заключении перечисляются основные результаты работы.
Основные результаты работы:
- Разработано единое промежуточное графовое представление для моделирования потока управления и потока данных: Размеченные графы анализа потоков работ.
- Для унифицированного анализа блочно-графовых языков описания потоков работ разработаны алгоритмы двустороннего отображения между созданным промежуточным графовым представлением и блочно-графовым базисным Формальным языком описания потоков работ, а также алгоритмы двустороннего отображения между Формальным языком описания потоков работ и языком BPEL.
- Созданы новые эффективные алгоритмы верификации и оптимизации потока работ, анализирующие произвольные структуры Размеченного графа анализа потока работ.
- Было доказано, что «функциональность» Размеченных графов потоков работ, не содержащих структурных конфликтов и удовлетворяющих некоторым дополнительным условиям, не изменяется при сохранении зависимостей по данным и управлению (условий выполнения заданий и вершин выбора). Таким образом, была предложена теоретическая основа для эквивалентных преобразований потоков работ.
- Была разработана Система автоматической верификации и оптимизации Размеченных графов анализа потоков работ, в которой были реализованы предложенные алгоритмы.
- Был создан прототип Системы управления электронной библиотекой «Научное наследие России», который исполняет BPEL-процессы, координирующие работу библиотеки. Был произведен анализ этих процессов.
По теме диссертации опубликованы следующие работы:
- Нестеренко А.К., Данилина А.А., Сысоев Т.М., Бездушный А.Н., Серебряков В.А. Автоматизация процессов интеграции распределенных информационных ресурсов // Электронные библиотеки: перспективные методы и технологии, электронные коллекции: Труды VIII всероссийской научной конференции. /Ярославский государственный университет им. П.Г. Демидова. – Суздаль, 2006. – С. 279-290.
- Данилина А.А. Автоматическая оптимизация потоков работ // Современные проблемы фундаментальных и прикладных наук: Труды 51-й научной конференции МФТИ. /МФТИ.– Москва-Долгопрудный, 2008.– Ч.VII,Т.3 – С.88-90.
- Каленкова А.А. Операционная семантика потоков работ // Информационные технологии и системы: наука и практика: Труды IV международной конференции. /Владикавказский научный центр РАН и Правительства Республики Северная Осетия — Алания – Владикавказ, 2009 – Ч.2 – С. 108-111.
- Каленкова А.А. Оптимизация потоков работ по времени выполнения, основанная на удалении избыточных потоков управления // Труды МФТИ, 2009. – Т.1, №. 2 – С.160-175.
- Каленкова А.А. Метод верификации потоков работ, основанный на построении логических выражений // Современные проблемы фундаментальных и прикладных наук: Труды 52 научной конференции МФТИ. /МФТИ.– Москва-Долгопрудный, 2009. – Ч.VII,Т.2 – С.125-128.
- Каленкова А.А., Серебряков В.А., Бездушный А.Н. Система автоматической верификации и оптимизации потоков работ // Телематика: Труды XVII всероссийской научно-методической конференции. /Санкт-Петербургский государственный университет информационных технологий механики и оптики. – Санкт-Петербург, 2010. – С. 381-382.
- Каленкова А.А. Применение условной конверсии для верификации и оптимизации потоков работ // Программирование – 2010. – Т.36, №. 5 – С.38-53.
- Каленкова А.А. Использование системы автоматической верификации и оптимизации потоков работ для анализа процессов обработки информационных ресурсов в электронной библиотеке // Распределенные информационно-вычислительные ресурсы" (DICR'2010). / Институт вычислительных технологий СО РАН. – Новосибирск, 2010. – С. 17.
