В последнее время широкое распространение в области верификации получил метод Model Checking [1, 2], или метод проверки на моделях. Суть его заключается в верификации свойств системы, представленных в виде формул временных логик LTL или CTL [3, 4]. При этом верифицируемая модель может быть задана либо явно – путем перечисления всех состояний и соединяющих их ребер, либо неявно – путем задания булевых функций, определяющих отношение переходов и множество начальных состояний. Однако при верификации больших информационных систем, в том числе и распределенных программных систем, зачастую приходится иметь дело с крайне большим числом состояний вычислительного процесса для их моделей. Например, для программы, одновременно выполняющей 10 потоков, каждый из которых может находиться в одном из 5 состояний, общее число состояний вычислительного процесса может достигать 510 = 9765625. Данная проблема называется комбинаторным взрывом и может стать непреодолимым препятствием на пути верификации тех или иных ее свойств.

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

Инструмент формальной верификации Spin

Spin, или Simple Promela Interpreter – инструмент формальной верификации для анализа корректности больших распределенных программных систем c конечным числом состояний. Модели анализируемых систем в Spin задаются в виде взаимодействующих асинхронных процессов, а формальная спецификация проверяемых условий – формулами LTL. Система Spin, как видно из названия, базируется на C-подобном языке Promela.

Promela, или Protocol Meta Language – язык для моделирования распределенных программных систем в виде взаимодействующих асинхронных процессов. Задача его – предоставление пользователю возможности построения модели распределенной программной системы и ее последующей проверки относительно всех аспектов работы и взаимодействия параллельных процессов, в связи с чем в языке существуют только три типа объектов спецификации: процессы, каналы обмена данными, переменные простых типов.

Также в языке Promela есть возможность задания требований к системе в виде формул времен- ной логики LTL, а в Spin предусмотрена возможность их быстрой интерпретации в автоматы Бюхи. Следует заметить, что все формулы логики LTL в Spin и Promela лишены оператора X (neXt), который определяет состояние системы в следующий момент времени.

Система Spin также предоставляет пользователю следующие опции для ускорения процесса верификации: редукция частичных порядков [5], абстракция данных [5], хэширование битовых состояний (вместо полных состояний хранится лишь их хэш, что снижает требования к объему памяти и уменьшает полноту системы) [6], ускорение проверки «корректности в слабом смысле», или Weak Fairness [7].

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

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

С 1995 года регулярно проводятся семинары Spin для пользователей данной системы и просто для тех, кто занимается исследованиями в области верификации больших распределенных програм- мных систем. В 2001 году Ассоциация вычислительной техники (ACM) вручила автору Spin награду System Software Award, что лишь подтвердило практическую значимость данной системы.

Распределенная верификация в Spin. На сегодняшний день для верификатора Spin, помимо простого последовательного алгоритма, разработано несколько распределенных алгоритмов анализа, которые позволяют ускорять процесс верификации для больших распределенных программных систем:

-      распределенный поиск в глубину, или Multi-Core Depth-First Search;

-      распределенный поиск в ширину, или Multi-Core Breadth-First Search.

Более подробно принцип работы данных алгоритмов рассматривается в [8, 9]. В этих работах описано тестирование пяти программных систем, для которых выполнен как последовательный, так и распределенный анализ данных систем без верификации конкретных свойств. Наилучшие результаты показал алгоритм поиска в ширину (рис. 2).

Серой пунктирной линией (linear) на рисунке 2 обозначено предельно возможное ускорение, которое соответствует числу используемых вычислительных узлов (CPUs).

Эффективность описываемых алгоритмов, как заявляют авторы представленных работ, прямо пропорциональна числу анализируемых состояний модели и в идеальном случае коэффициент ускорения может составить порядка 99 % от числа используемых вычислительных узлов. Однако при достаточно больших размерах тестируемых выше моделей систем, измеряемых миллионами состояний, фактически коэффициент ускорения остается весьма далеким от числа используемых вычислительных узлов. Так, например, для модели алгоритма телефонной коммуникации TPC ускорение на тридцати одном вычислительном узле не превысило значения 10, хотя число состояний модели было более 32 миллионов. А алгоритм Петерсона для взаимного исключения четырех взаимодействующих процессов на четырех вычислительных узлах показал ускорение всего в 2.3041 раза.

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

Таблица 1

Ускорение для распределенного алгоритма поиска в ширину

Table 1

Breadth first search distributed algorithm activation

№	Состояние		Ускорение
	Модель	Условие	1 CPU	2 CPUs	3 CPUs	4 CPUs
1	4	4	1.0537	0.0118	0.0116	0.1057
2	8	4	0.3174	0.0070	0.0041	0.0204
3	16	4	0.3028	0.0077	0.0039	0.0090
4	32	4	0.2347	0.0090	0.0080	0.0452
5	64	4	0.3031	0.0220	0.0183	0.0457
6	128	4	0.3253	0.0338	0.0470	0.0454

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

Для наиболее полного представления работы распределенного алгоритма в Spin автором была выполнена еще одна оценка. В ее основе был тот же алгоритм Петерсона для четырех процессов, только в данном случае его анализ уже проводился относительно следующего условия: «Если первый процесс начал свое выполнение, то когда-нибудь он войдет в критическую секцию». В целом было проведено десять тестов, для которых, помимо оценки ускорения распределенного алгоритма относительно последовательного, была также выполнена оценка времени, которое требуется на генерацию исходных кодов и их компиляцию. Результаты, представленные в таблице 2, показывают, что лишь анализ на основе четырех потоков в среднем позволяет получить ускорение, которое больше единицы, но совсем незначительно. Таким образом, для получения существенного ускорения в Spin для моделей относительно небольших разме- ров требуется выполнять анализ на значительно большем числе вычислительных узлов.

Дополнительную информацию по алгоритмам распределенного анализа в Spin можно найти в работах [10–12].

Распределенный алгоритм верификации автоматов Бюхи

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

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

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

Стоит отметить, что на данных этапах не происходит фактического построения синхронной композиции автоматов модели системы M (Model) и проверяемого условия W (Watchdog), а выполняется лишь процесс их синхронной работы, то есть посещение всех достижимых пар состояний из начальной пары , что позволяет существенно экономить расходуемую память.

Поиск допустимых состояний. Поиск допустимых состояний в композиции M и W начинается с поиска из их начальной пары состояний множества из таких N пар состояний-потомков, что любая непройденная пара состояний будет достижима хотя бы из одной пары состояний этого множества, где N – число используемых вычислительных узлов. Пример выбора состояний для двух произвольных различных случаев, где N=4, представлен на рисунке 3.

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

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

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

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

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

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

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

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

Рассмотрим пример суперлинейного ускоре- ния, достигаемого за счет первого этапа работы ал- горитма (рис. 4). 

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

Эффект суперлинейного ускорения может достигаться также и за счет второго этапа алгоритма (рис. 5).

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

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

Таблица 3

Распределенный алгоритм верификации автоматов Бюхи (все контрпримеры)

Table 3

A distributed algorithm of Buchi automata verification (all counterexamples)

№	Состояние		Ускорение
	Модель	Условие	1 CPU	2 CPUs	3 CPUs	4 CPUs
1	16	4	0.7329	1.0226	1.1638	1.0551
2	32	4	0.8735	1.2881	1.6484	1.8051
3	64	4	0.9645	1.5560	2.0014	2.3141
4	128	4	0.9726	1.6750	2.2571	2.7402
5	256	4	0.9844	1.7325	2.4244	2.8982
6	512	4	0.9808	1.7725	2.4883	3.0938

Таблица 4

Распределенный алгоритм верификации автоматов Бюхи (один контрпример)

Table 4

A distributed algorithm of Buchi automata verification (one counterexample)

№	Состояние		Ускорение
	Модель	Условие	1 CPU	2 CPUs	3 CPUs	4 CPUs
1	16	4	0.5773	1.1200	1.1089	0.8750
2	32	4	0.3745	0.4583	0.6037	0.5150
3	64	4	0.6663	0.6256	0.6274	0.5486
4	128	4	0.7689	1.0935	1.1832	1.0874
5	256	4	0.9206	1.5986	2.1694	2.5966
6	512	4	0.9379	1.6665	2.2660	2.7118

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

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

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

На рисунке 7 представлен график, позволяющий сопоставить оба подхода к поиску контрпримеров.

Сопоставление времен выполнения каждого из подходов показывает, что поиск всех контрпримеров длится в среднем в 6,5 раза дольше, чем поиск одного контрпримера при использовании того же числа потоков. Из рисунка 7 видно, что существенные отличия в ускорениях между данными подхо- дами возникают лишь при крайне маленьких раз- мерах модели (меньше 256 состояний). Это можно обосновать тем, что в случае поиска только одного контрпримера второй этап алгоритма дает значительно меньший прирост скорости, чем в случае поиска всех контрпримеров, поскольку его работа прекращается сразу же после нахождения любым из потоков допустимого состояния с циклом. А так как линейному алгоритму в случае с моделью не- большого размера на втором этапе нужно прове- рить лишь весьма малое число допустимых состояний на наличие циклов и не требуется тратить время на создание потоков, он оказывается более эффективным.

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

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

Сравнение со Spin

Проведем сравнительный анализ полученных данных об ускорениях распределенного алгоритма верификации автоматов Бюхи и распределенного алгоритма поиска в ширину в Spin. На рисунке 8 представлен график сравнения ускорений верификации для случайно сгенерированных автоматов.

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

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

Очевидно, что алгоритм распределенной верификации автоматов Бюхи является более эффективным с точки зрения демонстрируемого ускорения в зависимости от числа потоков. И хотя без учета этапов генерации и компиляции Spin демон- стрирует меньшее время выполнения, из графика, представленного на рисунке 9, видно, что верификация модели алгоритма Петерсона четырех процессов на пяти потоках у алгоритма распределенной верификации автоматов Бюхи займет меньше времени.

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

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

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

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

Литература

1.     Карпов Ю.Г. Model Checking. Верификация параллельных и распределенных программных систем. СПб: БХВ-Петер-бург, 2010. 552 с.

2.     Кораблин Ю.П. Семантика языков распределенного программирования: учеб. пособие; [под ред. В.П. Кутепова]. М.: Изд-во МЭИ, 1996. 102 с.

3.     Kroger F., Merz S. Temporal logic and State Systems. Springer, 2008, 436 p.

4.     Manna Z., Pnueli A. The temporal logic of reactive and concurrent systems: specification. 1992, 427 p.

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

6.     Holzman G.J. An analysis of bitstate hashing. Proc. 15th Intern. Conf. Protocol Specification, Testing, and Verification, 1998, pp. 301–314.

7.     Olderog E.-R., Apt K.R. Fairness in parallel programs: the transformational approach. ACM Transactions on Programming Languages and Systems, 1988, vol. 10, no. 3, pp. 420–455.

8.     Holzmann G.J., Bosnacki D. The design of a multi-core extension of the SPIN model checker. IEEE Transactions on Software Engineering, 2007, vol. 33, iss. 10, pp. 659–674.

9.     Holzmann G.J. Parallelizing the Spin Model Checker. Series Lecture Notes in Comp. Sc., 2012, vol. 7385, pp. 155–171.

10.  Barnat J., Brim L. Parallel breadth-first search LTL model-checking. Proc. 18th IEEE Intern. Conf. on Automated Software Engineering (ASE'03), 2003, pp. 106–115.

11.  Barnat J., Brim L. Distributed LTL model-checking in SPIN. Lecture notes in comp. sc., 2001, vol. 2057, pp. 200–216.

12.  Lerda F., Sisto R. Distributed-memory model checking with SPIN. Lecture notes in comp. sc., 1999, vol. 1680, pp. 22–39.