Software & Systems

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

Метод проверки модели является удобным инструментом при поиске ошибок в параллельных программных системах, однако его использование может быть ограничено из-за сложности реальных параллельных программных систем. Обычно данные системы состоят из нескольких частей, ра- ботающих асинхронно и разделяющих общие ресурсы. Исходя из этого, размер пространства состояний всей системы будет равен произведению размеров пространств состояний частей, входящих в систему [1]. Итоговая величина может достигать 10120 [2]. В связи с этим необходима оценка сложности проведения верификации параллельных программных систем с использованием метода проверки модели. В [3] дается общая оценка сложности проверки модели с использованием темпоральной логики линейного времени (LTL). В настоящей работе рассматривается сложность проверки модели с использованием LTL параллельных программных систем.

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

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

Метод проверки модели основан на использовании одной из основных темпоральных логик: CTL, LTL или CTL*. CTL является логикой ветвящегося времени, в которой рассматриваются различные пути вычислений программы. В отличие от CTL в LTL рассматривается единственный путь вычисления программы [2]. Логика CTL* является расширенной темпоральной логикой ветвящегося времени и объединяет в себе LTL и CTL. В данной работе рассматривается проверка с применением темпоральной логики линейного времени, что в совокупности с некоторыми ограничениями позволяет чередованием моделировать параллельные вычислительные системы.

Рассмотрим программную систему P, состоящую из n модулей P1, P2, …, Pn. Каждый из мо- дулей Pi работает параллельно с остальными модулями и выполняет отдельный процесс Пi программной системы P. Состояние системы определяется вектором значений общих переменных V={v1, v2, …, vm} и точкой управления в программе [4]. Вектор значений общих переменных V хранится в общей памяти M. Для того чтобы обратиться или сохранить значение переменной, процесс Пi должен получить доступ к памяти. В дополнение к этому каждый из процессов обладает своим набором частных переменных. Они используются для хранения результатов промежуточных вычислений или данных, не используемых другими процессами.

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

Область определения переменных програм- мной системы чаще всего является бесконечной, следовательно, она имеет бесконечное количество состояний. При проверке модели параллельной программной системы требуется, чтобы она имела конечное количество состояний. Для этого используются представления первого порядка: каждой переменной v∈V сопоставляется значение из множества D, называемого областью интерпретации [2]. Если множество D будет содержать только два элемента {true, false} или {0, 1}, то и P(v) сможет принять только значение true либо false. Таким образом, состояние – это оценка s: V→D для множества переменных из V.

Используя данный подход, можно сказать, что модель последовательной программы с помощью представлений первого порядка может быть описана структурой Крипке K=(S, S0, R, L), где S – конечное множество состояний программы; S0 – конечное множество начальных состояний программы; R: S×S – тотальное отношение переходов, то есть для каждого состояния s∈S должно существовать такое s'∈S, что (s, s')∈R; L: S→2AP – функция пометок, присваивающая каждому состоянию набор атомарных высказываний, истинных в данном состоянии.

Рассмотрим бесконечную последовательность состояний σ=s0, s1, …, где s0∈S0 и (si, si+1)∈R при i≥0. Такая последовательность σ является вычислением программы. Модель программы K удовлетворяет формуле темпоральной логики линейного времени φ, если все вычисления K удовлетворяют формуле φ.

Из структуры Крипке можно построить автомат Бюхи A=(Σ, S, S0, R, F), где Σ – конечное множество, которое называется алфавитом автомата A; S – конечное множество состояний автомата A; S0 – конечное множество начальных состояний (в случае детерминированного автомата содержит только один элемент); R – отношение переходов (для детерминированного автомата R: S×Σ→2S); F – множество допускающих состояний [3].

Таким образом, для модели K программы с конечным числом состояний и формулы φ проверка модели состоит в подтверждении того, что все последовательности, допускаемые автоматом АK, удовлетворяют формуле φ. Известно, что можно построить автомат Аφ, принимающий только те последовательности, которые удовлетворяют формуле φ [3]. Таким образом, проверка модели сводится к проверке того, что все состояния, принимаемые автоматом АK, принимаются и автоматом Aφ. Соответственно:

.                                               (1)

Автомат получается путем построения автомата . Количество состояний в этом автомате будет равно 2O(|φ|). Чтобы получить пересечение этих автоматов, можно использовать следующий результат: из двух автоматов Бюхи A=(Σ, S, S0, R, F) и B=(Σ, S¢, S0¢, R¢, F¢) можно построить автомат, принимающий L(A)ÇL(B). Такой автомат имеет |S|∙|S′| состояний. Зная, что автомат AK имеет |S| состояний, а автомат Aφ имеет 2O(|φ|) состояний, получаем, что автомат имеет |S|∙2(O|φ|) состояний. Таким образом, проверка того, что программа удовлетворяет формуле φ, будет выполнена за время

                                                       (2)

или в пространстве

.                                              (3)

Следовательно, задача относится к классу PSPACE [5]. Это означает, что проверка модели может быть выполнена с полиномиальным ограничением пространства.

Применим данный результат к параллельной программной системе P. Тогда каждый из n ее процессов Пi описывается структурой Крипке Ki=(Si, S0i, Ri, Li). При параллельной работе процессов используется моделирование чередованием с применением правил, описанных выше. При моделировании необходимо выполнить требование справедливости, то есть запрет на бесконечные последовательности состояний, определяемые только одним из n процессов. В таком случае для параллельной программной системы

; ;

; (s, s′)ÎR,

если и только если (s[i], s′[i])ÎRi.

Сложность проверки модели параллельной программной системы P определяется относительно размера модулей Pi, из которых состоит система, и длины проверяемой формулы.

Как отмечено выше, размер пространства состояний всей системы будет равен произведению размеров пространств состояний частей, входящих в систему |S|=|S1|∙|S2|∙…∙|Sn|. Подставляя данное выражение в формулы (2) и (3), для параллельной программной системы, состоящей из n модулей, получаем соответственно:

,                             (4)

.  (5)

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

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

Литература

1.     Vardi M.Y. Linear vs. Branching Time: A Complexity-Theoretic Perspective. In Proc. Logic in Computer Science. Thirteenth Annual IEEE Symposium. 1998, pp. 394–405.

2.     Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking; [пер. с англ.; под ред. Р. Сме­лянского]. М.: МЦНМО, 2002. 416 с.

3.     Vardi M.Y., Wolper P. An automata-theoretic approach to automatic program verification. In Proc. First Symposium on Logic in Computer Science, Cambridge, 1986, June, pp. 322–331.

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

5.     Sistla O.A.P., Clark E.M. The Complexity of Propositional Linear Temporal Logics. Journal ACM. 1985. № 32, pp. 733–749.