Abstract

Abstract

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

Full Text

Концептуальную основу программирования последовательных вычислений составляет понятие алгоритма, реализуемого по шагам строго последовательно во времени. В противоположность этому параллельная программа порождает совокупность одновременно протекающих процессов обработки информации, полностью независимых или связанных между собой статическими или динамическими пространственно-временными или причинно-следственными отношениями. Параллельное программирование, суть которого заключается в использовании преимуществ многоядерных или многопроцессорных компьютеров – разделении процесса на несколько выполняющихся «параллельно» потоков, сложнее реализовывать, чем последовательное, поэтому его необходимо подвергать строгому анализу и проверке с помощью различных методов верификации. Классические методы верификации Р. Флойда [4], Ч. Хоара [5] и Э. Дейкстры [3] рассчитаны на императивные однопоточные программы. Тем не менее, эти проверенные временем методы можно использовать в параллельном программировании, подвергнув некоторым модификациям. Книга Ю.Г. Карпова [2] в данном случае подходит не в полной мере, потому что там рассматривается метод формальной верификации model checking, для применения которого система представляется в виде переходов с конечным числом состояний. Здесь же не рассматривается множество состояний, переходы и разметка в качестве основы верификации [2]. Для верификации программы необходимо задаться критерием ее правильности – спецификацией – средством для точного описания того, что должно быть совершено в результате выполнения программы. Спецификация по Дейкстре [1, 3] задается с помощью двух предикатов: предусловие {Q} и постусловие {R}. Таким образом, сама спецификация также является предикатом {Q} S {R}, который истинен: если выполнение программы S началось в состоянии, удовлетворяющем Q, то оно завершится через конечное время в состоянии, удовлетворяющем R. Слабейшим предусловием является условие, характеризующее множество всех начальных состояний, при которых выполнение обязательно приведёт к правильному завершению, причём система останется в конечном состоянии, удовлетворяющем заданному постусловию. Оно обозначается wp(S,R) [3]. При доказательстве правильности цикла, кроме пред- и постусловия, используются инвариант и ограничивающая функция. Инвариант P – логическое выражение, описывающее зависимости переменных цикла. Оно должно быть истинно после каждого прохода тела цикла и перед началом выполнения цикла. Аннотированный цикл должен выглядеть следующим образом: do B1 ® S1 B2 ® S2 … Bn ® Sn od где B – служит охраной входа (®) – условие; S – выполняется только при истинности B; B®S – охраняемая команда;  – равнозначно elseif – команде выбора, разделитель вариантов; do…od – оператор из набора охраняемых команд. Если нет ни одной охраны с истинным значением, происходит правильное завершение программы, но при этом работе нельзя завершиться, пока хотя бы одна охрана является истинной. По теореме о цикле [1, 3] для проверки существует ряд условий: 1. P истинно перед выполнением цикла {Q} – начальная инициализация переменной {P}. 2. P является инвариантом цикла {P&Bi}Si{P}. (1) 3. Выполнение P и невыполнение BB должны дать R: P&BBR. 4. Если цикл еще не закончен, то ограничивающая функция положительна: P & BB t > 0. 5. Каждый шаг цикла ведет к концу цикла {P & Bi} t1:=t;S1 {t<t1}. Для применения метода Дейкстры происходит выделение в параллельной программе слоёв за счёт разбиения на последовательность операторов каждого её процесса. При этом первым слоем будут считаться все те операторы, которым требуются только входные параметры и константы. После того как эти операторы окажутся вычисленными, на следующем шаге для вычисления выбираются все те операторы, которые имеют на своем входе вычисленные данные; таким образом формируется следующий слой [6]. Порядок выполнения данных слоёв не важен, поскольку взаимодействие процессов происходит только внутри них, то есть слои являются коммуникационнозамкнутыми. Программа называется безопасной, если все её слои коммуникационно-замкнутые. В этом случае вместо верификации всей параллельной программы можно проводить её послойную верификацию – последовательное доказательство вход-выходных соотношений для каждого слоя. Иными словами, каждый слой представляет собой последовательную программу [7], к которой применим метод Дейкстры, что было неоднократно доказано. Рассмотрим применение метода Дейкстры для верификации параллельной программы, вычисляющей значение через сложение и умножение. Следует учесть, что данный пример можно реализовать и при помощи последовательного алгоритма. Первый этап построения программы – составление спецификации. (2) Сначала построим последовательную программу. По постановке задачи, очевидно, что в программе будет цикл. Для этого спецификация должна быть дополнена инвариантом P и ограничивающей функцией t: (3) Построенная, исходя из спецификации, программа приведена на листинге 1: Листинг 1 Выполним один из элементов верификации – проверку цикла по формуле (1) Дейкстры – проверка инварианта. (4) Импликация истинна, поскольку: Преобразуем последовательную программу в параллельную таким образом, чтобы она порождала три процесса: 1. Процесс вычисления . 2. Процесс вычисления . 3. Процесс вычисления . Листинг 2 Здесь: - !a передача в канал a значения переменной a, - !b передача в канал b значения переменной b, - ?a получение из канала a значения переменной a, - ?b получение из канала b значения переменной b. Для анализа параллельной программы построим сеть Петри для порождаемых ее процессов (рисунок). Рис. Сеть Петри На рисунке: - места маркируются операторами присваивания, - переходы названиями каналов, - немаркированные места/переходы использованы для соответствия правилам построения сетей Перти, - дуги промаркированы только в случаях недетерминизма в выборе перехода. Заданный для последовательной программы (листинг 1) инвариант P должен выполняться в параллельной программе (листинг 2) после места на рисунке, маркированного как «». Тело цикла последовательной программы в параллельной программе состоит из двух коммуникационно-замкнутых слоев: первому слою цикла соответствуют места (см. рисунок), маркированные как «» и «», второму слою – «». Таким образом, спецификацию для выполнения команд, входящих в коммуникационно-замкнутые слои цикла, по аналогии со второй проверкой цикла Дейкстры можно записать в следующем виде: <команды 1-го слоя>;<команды 2-го слоя>{P}. В инвариант, по сравнению с использованным в последовательной версии, необходимо добавить соотношение между счетчиками циклов. Команды первого слоя, как выполняющиеся одновременно и независимо, можно подставить в формулу в любом порядке. Важно, что команды второго слоя должны строго следовать за командами первого. После этих преобразований можно воспользоваться обычной формулой Дейкстры для доказательства правильности спецификации: Доказывается истинность импликации аналогично варианту с последовательной программой (4). В примере рассмотрена самая важная и сложная проверка цикла – на сохранение инварианта. Остальные проверки строятся аналогично.