ПРОГРАММИРОВАНИЕ, 2010, No 5, с. 38-53
ТЕСТИРОВАНИЕ, ВЕРИФИКАЦИЯ И ВАЛИДАЦИЯ ПРОГРАММ
УДК 004.92+004.94
ПРИМЕНЕНИЕ УСЛОВНОЙ КОНВЕРСИИ ДЛЯ ВЕРИФИКАЦИИ И ОПТИМИЗАЦИИ ПОТОКОВ РАБОТ
© 2010 г. А. А. Каленкова
Вычислительный центр РАН 119991 Москва, ул. Вавилова, 40 E-mail: akalenkova@ultimeta.ru Поступила в редакцию 09.03.2010 г.
На основе предложенных нами ранее графов анализа потоков работ [1] и известного метода условной конверсии [2] создан новый алгоритм верификации потоков работ. Алгоритм использует булеву алгебру, что отражено в его названии - алгоритм булевой верификации (АБВ). АБВ работает с произвольными перекрывающимися структурами графа и циклами. Временная сложность предлагаемого алгоритма в случае с насыщенными графами не превышает таковую для большинства других алгоритмов верификации потоков работ [3-6]. В процессе верификации АБВ определяет условие выполнения каждой вершины графа, что дает возможность дополнительно создать алгоритм оптимизации потоков работ. В отличие от известных алгоритмов структурной оптимизации потоков работ, базирующихся на применении шаблонных преобразований [7, 8], предлагаемый алгоритм оптимизации позволяет максимально (в пределах цикла) распараллелить поток работ, содержащий произвольные перекрывающиеся структуры.
1. ВВЕДЕНИЕ
Потоком работ принято считать формальное описание процедуры передачи данных и управления между участниками бизнес-процесса в соответствии с некоторыми правилами. Бизнес-процесс, в свою очередь, представляет собой совокупность связанных между собой действий, которые совместно реализуют некоторую задачу бизнеса в рамках организационной структуры, описывающей функциональные роли и отношения. Потоки работ создаются и исполняются в системах управления потоками работ [9]. Несмотря на привязку определения потока работ к деятельности компаний, системы управления потоками работ могут быть предназначены для описания произвольных процессов интеграции географически распределенных данных и приложений. С распространением глобальной сети Интернет появилась возможность применения систем управления потоками работ для объединения информационных и вычислительных ресурсов различных организаций [10].
Бизнес-процессы могут иметь достаточно объемную структуру (содержать множество действий и подпроцессов), что обуславливает необходимость применения средств автоматической верификации и оптимизации потоков работ. На основе анализа бизнес-процессов было выделено несколько основных шаблонов потока управления, которые должны поддерживаться языками описания потоков работ [11]. Были предложены графические языки описания потоков работ, такие как Workflow nets и Workflow graphs [3], реализующие шаблоны потока управления, они позволили создать ряд алгоритмов верификации [3-6] и распараллеливания [7, 8] потоков работ.
Представленные в литературе алгоритмы структурной оптимизации потоков работ [7, 8] имеют недостаток - невозможность анализа и трансформации произвольных перекрывающихся структур графов, описывающих потоки работ. Мы предположили, что множество заданий некоторого экземпляра потока работ и порядок их выполнения определяются значениями условий в вершинах выбора графа, исходя из этого, мож-
Рис. 1.
но построить алгоритмы верификации и оптимизации, работающие с произвольными перекрывающимися структурами. На основе введенного нами ранее определения графов анализа потоков работ [1] мы разработали алгоритм булевой верификации (АБВ) графов анализа потоков работ и алгоритм последующей оптимизации, который использует полученные в ходе верификации условия выполнения вершин. АБВ базируется на уже известном в теории компиляторов алгоритме условной конверсии [12], который определяет условия выполнения команд программы. Особенность предлагаемого в статье алгоритма (АБВ) заключается в работе с дополнительными распараллеливающими и синхронизирующими конструкциями. Как и алгоритм условной конверсии для "привычных" языков программирования [2], АБВ может быть построен так, что время его работы будет полиномиально.
2. ГРАФ АНАЛИЗА ПОТОКА РАБОТ
В работе [1] для формализации потоков работ нами были предложены граф анализа потока работ и размеченный граф анализа потока работ.
Определение 1. Графом анализа потока работ (или просто графом анализа) называется шестерка ЛС = (Ж, Т, С, И, ^):
N
конечное множество вершин;
- T С N - конечное множество заданий;
- ts G T - начальное задание;
- C С N - конечное множество вершин выбора;
- M С N - конечное множество вершин слияния;
- F С N х N - поток управления.
При этом выполнены условия:
- у начального задания нет входящих дуг;
- для каждой вершины n G N существует путь из ts в n;
- у заданий, в отличие от других вершин, может не быть исходящих потоков управления;
- каждая вершина выбора имеет по крайней мере две исходящие дуги.
Граф анализа потока работ - это направленный граф, в котором вершины делятся на задания, выполняющие полезную работу, и координаторы выбора или слияния (рис. 1).
Как и сеть Петри (Petri net) [3], граф анализа обладает не только статической, но и динамической составляющей - дуги графа могут содержать некоторое количество фишек (tokens) или не содержать их вовсе. В отличие от сетей Петри, фишки располагаются не в вершинах графа, а на дугах. Перед началом исполнения потока работ исходящая дуга начального задания содержит одну фишку, остальные дуги графа не содержат фишек. Задание одновременно синхронизирует и разветвляет поток управления: ожидается появление фишек на всех входящих дугах, по одной фишке забирается с каждой дуги, далее задание выполняется и по одной фишке добавляется на каждую исходящую дугу. При выборе ожидается появление фишек на всех входящих дугах, по одной фишке забирается с каждой входящей дуги и добавляется по фишке на некоторые из исходящих дуг. И, наконец, при слиянии забирается фишка с одной из входящих дуг (если фишки есть на нескольких дугах, выбор недетермини-рован) и передается фишка на исходящую дугу. Исполнение потока работ завершается, когда ни одна вершина не может быть активирована.
Введем ряд обозначений: Id - это множество идентификаторов, Str - множество строк, Boolean = {true, false}, знак ^ задает частичную
функцию. Для символов, формирующих идентификаторы и строки, допускается использование различного набора индексов. Через Vin и Vout обозначим множества векторов произвольной конечной длины с координатами из множества Id и введем понятие размеченного графа анализа.
Определение 2. Размеченным графом анализа потока работ (или просто размеченным графом анализа) называется кортеж LAG = = (N,T,ts,C, M, F, Lt, Lin , Lout, Lch, Lcond, Lf):
- (N, T, ts, C, M, F) - граф анализа;
- Lt G (T\{ts} ^ Id) - каждому заданию (за исключением начального задания) ставится в соответствие его название;
- Lin G (T\{ts} U C ^ Vin - некоторым заданиям и некоторым вершинам выбора ставится в соответствие список входных параметров;
- Lout G (T\{ts} ^ Vout - некоторым заданиям ставится в соответствие список выходных параметров;
- Lch G (C ^ Str) - каждой вершине выбора ставится в соответствие условие выбора;
- Lcond G (F' ^ Boolean), F' Ç F, f' = (ni,U2) G G F1 ^ ni G C - всем потокам управления, исходящим из вершин выбора, ставится в соответствие условие, при этом Vc G C fi, f2 : Lcond ( fi ) = true, Lcondf) = false, то есть из каждой вершины выбора исходят дуги, как с пометкой Lcond = true, так и с пометкой Lcond = false;
- Lf G (F ^ Id U {'&'}) - некоторым потокам управления ставится в соответствие идентификатор или амперсанд.
Фактически размеченный граф анализа - это граф анализа, дополненный некоторыми пометками. Вершина выбора размеченного графа анализа передает фишки на все дуги с пометкой Lcond = true или на все дуги с пометкой Lcond = = false, остальные вершины срабатывают так же, как в графе анализа потока работ. Семантика размеченного графа анализа потока работ [1] похожа на семантику сети Петри (Petri net) и сети потока работ (Workflow net), но более всего
она схожа с семантикой графа потока работ (Workflow graph) [3]. Размеченный граф анализа потока работ реализует некоторые конструкции потока управления более компактно, чем граф потока работ, в силу того, что задания и вершины выбора одновременно распараллеливают и синхронизируют поток управления. С другой стороны, шаблон исключающего выбора [11] в случае трех или более альтернатив реализуется не с помощью одной вершины выбора, как это делается в графах потоков работ, а с помощью нескольких вершин выбора размеченного графа анализа. Однако условия выполнения вершин и активации дуг в размеченном графе анализа могут быть определены с помощью булевых функций над множеством идентификаторов вершин выбора.
Размеченный граф анализа позволяет указать в качестве входных и выходных параметров глобальные переменные потока работ и дает возможность анализировать зависимости по данным. Можно предложить метод описания семантики потока работ с различными уровнями видимости переменных в виде размеченного графа анализа.
Отметим, что не все пометки размеченного графа анализа, такие, как названия заданий, дуг и условия выбора, будут использованы в предлагаемых алгоритмах, они нужны лишь для полного описания потока работ так, чтобы после оптимизирующих преобразований его можно было записать на одном из языков определения потоков работ [13-15].
3. АЛГОРИТМ БУЛЕВОЙ ВЕРИФИКАЦИИ (АБВ) И АЛГОРИТМ ОПТИМИЗАЦИИ ПОТОКОВ РАБОТ
3.1. Определение зависимостей по управлению в потоках работ
Зависимость по управлению между операторами программы неформально определяется как наличие порядка выполнения этих операторов, нарушение которого может привести к изменению результата работы программы [12]. Так, например, оператор, находящийся под управлением оператора условного перехода, не может быть выполнен раньше, чем будет вычислено
выражение, которое определяет условие перехода. Для оценки возможности векторизации последовательных программ применяется метод условной конверсии [12], основной идеей которого является преобразование всех операторов, находящихся
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.