9.3. Модель параллельных процессов

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

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

Переход вместе с инцидентными ему вершинами (местами) изображен на рис. 9.1.

Рис. 9.1. Переход а и инцидентные ему вершины (места)

На рисунке обозначено: множество локальных индивидуальных и пропозициональных переменных, условие, при истинности которого и активном месте происходит выполнение перехода а из места в место действие или константа перехода преобразование, ассоциируемое с этим действием. Если место активно и истинно, то говорят, что переход а является допустимым для Место может иметь к инцидентных ему переходов (рис. 9.2).

Рис. 9.2. Совокупность переходов к

Полным входным условием для места является При этом , если и не требуется, чтобы Такие процессы называют обычно детерминированными. Если процесс имеет хотя бы один переход а, который является допустимым, то процесс Р называют допустимым.

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

Часто будем представлять процесс в текстовой линейной форме вместо графовой. Каждый переход и инцидентные ему вершины будем представлять одним предложением, называя его иногда командой. Приведем примеры предложений в текстовой форме и соответствующие им графы (рис. 9.3, 9.4), являющиеся частным случаем графического представления переходов, приведенных на рис. 9.1, 9.2:

Рис. 9.3. Переход, соответствующий (9.2)

Рис. 9.4. Переход, соответствующий (9.3)

Последнее предложение содержит программный сегмент деталями которого мы не интересуемся. Существенным для нас является только следующее:

1) сегмент может изменять только переменные и может использовать для этого только переменные

2) выполнение сегмента должно обязательно завершиться.

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

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

(см. скан)

(см. скан)

Как видно из приведенного описания, процесс Числитель, последовательно используя значения равныел, вычисляет числитель в Процесс Знаменатель, используя значения последовательно равные

, вычисляет знаменатель, присваивает значения а затем делит на Предложения

синхронизируют выполнение процесса (Знаменатель) с процессом (Числитель), чтобы обеспечить деление на только после того, как оно будет умножено на без остатка. Основанием этому служит теорема, утверждающая, что произведение последовательных чисел к всегда делится на Рассмотрим теперь, как параллельные процессы вычисляются. Вместо понятия «вычисление» будем использовать понятие «выполнение» как соответствующее понятию процесса.