Параллельное программирование. Программирование взаимодействующих процессов

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

Асинхронное программирование
Асинхронная модель вычислений наиболее пригодна для описания вычислений на мультипроцессоре и/или мультикомпьютере. Асинхронная программа определяет систему независимо исполняющихся и взаимодействующих процессов. Существует много различных воплощений этой модели вычислений в различных языках программирования. Здесь эта модель рассматривается в самом общем виде.

Асинхронная программа (А-программа) - это конечное множество А-блоков {Ak |k∈{1,2,...,т}} определенных над информационной IM и управляющей CM памятями.
Каждый А-блок Ak=
состоит из спусковой функции tr(ak) (trigger function), операции ak, ak∈F и управляющего оператора c(ak).
Памятью называется конечное множество ячеек памяти, способных хранить значения переменных.
Спусковая функция tr(ak) - это предикат, в программе обычно задается условным выражением либо логической функцией. Как обычно здесь, операция ak реализуется в программе одноименной процедурой, вычисляющей функцию fa.
Понятие асинхронной программы

Управляющий оператор c(ak) - оператор присваивания или процедура, меняющая значения ячеек управляющей памяти CM (например, чтобы разрешить или запретить исполнение какого-нибудь А-блока).
Каждой переменной из in(ak)∪out(ak) в памяти IM соответствует ячейка, в которой хранится ее значение.
Выполнение А-программы состоит:
в вычислении значения спусковой функции tr(ak) для всех, части А-блоков или ни одного,
в выполнении ни одного, части или всех А-блоков Ak таких, что tr(ak)=true при текущем состоянии памяти IM∪CM.

Таким образом, исполняющая система в зависимости от имеющихся в наличии свободных на этот момент ресурсов имеет право инициировать любое подмножество А-блоков, готовых к исполнению (с истинной tr(ak)). Понятно, что при разных исполнениях асинхронной программы на каждом этапе исполнения будут инициированы, вообще говоря, разные подмножества А-блоков. Это обстоятельство (недетерминизм исполнения А-программы) сильно усложняет отладку асинхронной программы.

Выполнение А-блока Ak состоит в исполнении:
процедуры ak с теми значениями, которые имеют переменные из in(ak) в текущий момент, при этом вычисляются значения переменных из out(ak),
управляющего оператора c(ak).
Следовательно, спусковые функции и управляющие операторы - это те средства, с помощью которых задается управление в асинхронных программах .
А-программа считается завершенной, когда ни один блок не выполняется и ни один А-блок не может быть инициирован, так как для всех к=1,...,m значение tr(ak)=false .

П1

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

П2.Большая непроцедурность часто мешает эффективно выполнить программу и в таких случаях требуется уменьшать непроцедурность программы (представления алгоритма), сделать управление более жестким, более определенным, не оставляющим места на размышления в ходе вычислений. Для программы примера П1 это можно сделать, убрав дизъюнктивные члены из спусковых функций, что усилит управление (увеличит множество ограничений в нем).
integer x, y, z;
input (x,y,z)
asynchronous_do
tr(ak) ak
x
y
z
end_do

П3.Программа нижеследующего примера отличается от программы примера П2 тем, что в спусковые функции добавлены новые конъюнктивные и дизъюнктивные члены. Они добавляют новые ограничения в управление и в результате получается почти последовательная программа. Параллельное выполнение двух А-блоков возможно лишь при условии равенства значений двух переменных (при равенстве значений всех трех переменных программа завершается).
input (x,y,z)
asynchronous_do
tr(ak) ak
x
y
z
end_do

П4.В примерах П1 - П3 А-блоки не имели управляющего оператора (более точно, был пустой управляющий оператор). Рассмотрим теперь организацию конвейерного исполнения А-блоков. Схема программы показана на рис. 4.2.
Рис. 4.1. Рис. 4.2.

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

В этой программе операторы присваивания x:=1; y:=z:=0; значений управляющим переменным разрешают инициировать операцию f1 и запрещают инициирование операций f2 и f3. Таким образом, в начальный момент времени сможет быть инициирован только А-блок f1. После выполнения операции f1 управляющий оператор с1 (здесь это оператор [y:=1; x:=0]) запретит исполнение А-блока f1 и разрешит исполнение А-блока f2 и т.д. Цикл конвейера завершится, когда предикат P станет ложным и не позволит инициировать А-блок f3.
Асинхронное программирование оказалось весьма трудоемким делом, особенно отладка программы, в силу обилия возможностей совершить ошибки в синхронизации процессов. Рассмотрим некоторые проблемы асинхронного программирования.

Некорректное вычисление данных
Возникновение некорректных данных иллюстрирует следующий простой пример. Пусть необходимо начислить зарплату и вычислить сумму денег, подлежащих выдаче на руки. Оставляя в стороне излишние здесь детали, будем предполагать, что зарплату составляет некоторая базисная зарплата N0 плюс надбавки N1, N2, ... , Nn (выражаются в процентах к базисной зарплате) минус налог Nn+1 (выражаются в процентах к начисленной сумме).

Пусть процессы P0, P1, P2, ... , Pn, Pn+1 выполняют эти операции. Для вычисления корректного результата процесс Pn+1, вычисляющий сумму налога, должен выполняться последним, процесс P0 - первым, а процессы P1, P2, ... , Pn могут исполняться в любом порядке, хотя само суммирование должно, конечно, выполняться последовательно. Все другие варианты выполнения процессов приведут к некорректным результатам.
Такого сорта ошибки асинхронных программ крайне неприятны, трудно локализуемы и неповторимы. Если позволить процессам P1, P2, ... , Pn, Pn+1 выполняться асинхронно, то при разных выполнениях асинхронной программы могут получаться разные результаты и повторить предшествующее тестирование удастся только случайным образом. Понятно, что (P0 + P1 + Pn+1 + P2 + ... + Pn) ≠ (P0 + Pn+1 + P1 + P2 + ... + Pn), здесь имеется ввиду, что процессы выполняются в написанном порядке.

Следующий пример иллюстрирует этот тип ошибки. Пусть в банке А есть счет acc1, на котором находится 500 тыс. руб., а в банке B - счет acc2, на котором находится 300 тыс.руб, и необходимо переслать 100 тыс.руб. со счета acc1 на счет acc2. Сумма денег на обоих счетах неизменна до и после выполнения пересылки и равна 800 тыс. руб. Пусть процесс P1 посылает деньги из банка А в банк B, а процесс P2 принимает посланные деньги в банке B. Процессы схематически могут быть описаны так:
Некорректное считывание данных

Первоначально
А.acc1=500 тыс.руб.
В.acc2=300 тыс.руб.
Процесс P1 Процесс P2
А.acc1:=А.acc1 - 100; receive (x,A,y);
x := 100
send (x,B,y); B.acc2 := В.acc2 + y;
Результат
А.acc1=400 тыс.руб.
В.acc2=400 тыс.руб.

В процессе P1 счет А.acc1 вначале уменьшается на 100 тыс. руб., а затем 100 тыс. руб. посылаются в банк В. В процессе P2 сначала принимаются 100 тыс. руб. из банка А, а затем увеличивается сумма на счету В.acc2.
Однако процесс P, контролирующий перевод денег и проверяющий сохранение значения суммы А.acc1+B.acc2, может считывать ошибочные данные. Понятно, что если P будет считывать данные строго до или после выполнения операции перевода денег, то результат суммирования будет одинаков. Однако в ходе выполнения процессов P1 и P2 при разных вариантах считывания значений А.acc1 и B.acc2 сумма А.acc1+B.acc2 может равняться 700 тыс.руб. (если значение А.acc1 было считано после его изменения, а значение B.acc2 - до изменения) , 800 тыс.руб. и 900 тыс.руб. при других возможных вариантах считывания данных.

Широко известным примером реализации модели асинхронного программирования является message passing interface (MPI). Этот метод программирования определяет программу как систему взаимодействующих процессов и стандартизует обмен данными. Обмен всегда происходит через каналы, связывающие два процесса. Такой канал реализуется очередью сообщений, каждый процесс сам определяет свою готовность начать исполнение или завершить его.
В разных формах MPI изучался в асинхронных вычислениях с конца 60-х годов. В настоящее время MPI используется практически во всех коммерческих мультикомпьютерах в качестве основного средства параллельного программирования. Идеи программирования с MPI рассматриваются в самой общей форме.
Message passing interface

Предполагается, что программа определяется как система независимых, параллельно протекающих взаимодействующих процессов. Как обычно, здесь процесс - это исполняющаяся программа со всеми обрабатываемыми данными. Исполнение этой же программы с другими данными определяет другой процесс.
Взаимодействие определяется как посылка сообщения из одного процесса в другой и прием сообщения. Сообщение - любая последовательность битов, которая чаще структурируется и определяется как значение набора (кортежа, структуры) переменных. Сообщение посылается в в канал в одном процессе и выбирается из одноименного канала в другом процессе.
Канал может рассматриваться как очередь. Оператор send записывает сообщение в канал, в канале может накопиться очередь не выбранных сообщений. Оператор receive выбирает сообщение из канала, если оно есть в канале.
Определение MPI

В программе для использования MPI прежде всего следует описать каналы, например:
ch queue (<описание_переменной>)
Описание определяет канал queue, который в состоянии хранить значения переменной канала описанного типа. Переменная канала может быть простой или структурированной. Возможны описания вида:
ch symbol (char);
ch data (day, month, year : integer);
ch personal_date (name : string, age : integer );
Запись сообщения в канал производится оператором send.
send <имя_канала> (<выражение>);

Выражение должно вырабатывать значение переменной, описанной в определении канала. Например:
send data (d+1, m, y);
Переменные d, m и y определяются в процессе-отправителе и должны содержать целые значения, как это и определено в описании канала data.
Данные выбираются из канала оператором receive.
receive personal_date (n, a);
Переменные n и a определяются в процессе-получателе и должны быть описаны так же, как переменная канала. После выполнения оператора receive переменная n может содержать значение “Иванов И.И.”, а переменная a - значение “30”.

Если канал предполагается неограниченным (асинхронный MPI), то оператор send может быть выполнен неограниченно много раз (не блокируемый оператор).
Оператор receive получает значение из канала, если он не пуст. Если в канале нет значения, выполнение оператора receive задерживается (блокируемый оператор) до появления значения в канале.
Каналы описываются как глобальные объекты, поскольку они разделяются процессами программы. Можно определить массив каналов, например:
ch data [1:k](day, month, year : integer);
Допускается, чтобы несколько процессов посылали сообщения в один и тот же канал. Аналогично, несколько процессов могут получать данные из одного канала. Описанный канал в начальный момент пуст.

П1.Одно из типичных межпроцессных взаимодействий определяет взаимодействия клиента и производителя. Производитель создает продукт и продает его многим клиентам. Программа их взаимодействий может иметь вид.
ch request ( integer, <описание_запроса_клиента>);
ch reply (integer, <описание_результата>);
% <описание_запроса_клиента> - это описание типов переменных, значения которых специфицируют запрос клиента к производителю. Значение переменной, описанной как integer, определяет уникальный номер клиента.
<описание_результата> - описание переменных, специфицирующих ответ производителя на запрос клиента %

Producer :: var index, ...;
do true → receive request (index, ... ); % ожидание запроса клиента%
..... % обработка запроса клиента и формирование ответа%
send reply [index ] ( ... ); % ответ клиенту %
od;
Client [i : 1...n ] :: send request (i, ... );
% обращение к Producer %
receive reply [i ] ( ... ); % ожидание ответа Producer %

В программе определены n+1 независимых параллельно протекающих процессов: один процесс-производитель Producer и n процессов-клиентов Client. Именно так могут быть описаны взаимодействия файл-сервера и программ, запрашивающих (открывающих) нужные им файлы. При этом файл-сервер ответственен за то, чтобы только одна программа получала доступ к файлу по записи. Это же управление годится для программирования удаленного доступа к дисковому файлу нескольких программ в сети. Много подобных задач в разных вариантах возникает при организации обработки данных в сети.

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

Семафоры
Семафоры являются тем базовым средством, с помощью которого можно реализовать в программе управление параллельно протекающими процессами, их синхронизацию и взаимодействия.
Семафор S есть переменная типа integer, которая после инициализации начального значения доступна только посредством семафорных операций P (от голландского слова proberen - проверить) и V (от голландского слова verhogen - увеличить, прирастить). Никаким другим способом значение семафорной переменной не может быть ни проверено, ни изменено.
Операции P и V определяются следующим образом: P(S): while S ≤ 0 do skip; S:=S-1;
V(S): S:=S+1;

Каждая из операций P и V является неделимой, т.е. если семафорная переменная изменяется одной из операций, то в это время к ней нет доступа ни для какого процесса. Таким образом, изменение значения семафорной переменной (S:=S-1 или S:=S+1) может делаться только одной операцией (одним процессом). В определении семафорной операции P оператор цикла
while S ≤ 0 do skip;
описывает алгоритм выполнения операции P(S). В реализации операции P нет, конечно, необходимости циклить на этом операторе. Обычно операция P(S) реализуется таким образом, что если в процессе при выполнении операции P(S) удовлетворяется условие S≤0, то процесс переводится в состояние ожидания и вновь инициируется только по выполнению операции V(S) в любом из процессов.

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

Задача взаимного исключения
Взаимное исключение может быть реализовано с помощью семафоров следующим образом.
Пусть для n процессов Proc(i), i=1,2, ... ,n, должно быть обеспечено взаимное исключение при доступе к некоторому ресурсу (все равно какому). Для программирования взаимного исключения используется семафорная переменная mutex (mutual exclusion). Тогда структура программы i-го процесса такова:

var mutex=1: semaphore;
/* семафорная переменная mutex инициируется со значением 1 */
Proc(i) :
repeat
. . . /* начальная часть программы процесса*/
P(mutex)
. . . /*критический интервал*/
V(mutex)
. . . /* заключительная часть программы процесса */
until false

Программу процесса составляют операторы языка программирования, заключенные между операторами repeat и until. Логически программа процесса делится на три части. Участок программы процесса между операторами P(mutex) и V(mutex) называется критическим интервалом. Здесь выполняются те вычисления, ради которых затевалось взаимное исключение. Критический интервал “охраняется” семафором mutex от влияния других процессов. Действительно, если инициализировать семафорную переменную mutex значением 1, то только один процесс будет в состоянии выполнить операцию P и войти в свой критический интервал. Все остальные процессы будут ожидать на операторе while mutex ≤ 0 do skip;

Завершив выполнение критического интервала, процесс выполнит оператор V(mutex) и увеличит значение семафорной переменной mutex на единицу. Следовательно, один из ожидающих процессов (неизвестно какой) получит право войти в свой критический интервал.
Если инициировать семафорную переменную со значением, например, 3, то тогда 3 процесса получат право одновременно выполнять свои критические интервалы.

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

Заведем соответственно два семафора для описания этих состояний:
b_empty - содержит количество свободных позиций для размещения новых элементов данных в буфере, инициализируется значением n, и
b_full - содержит количество элементов данных в буфере, инициализируется значением 0.
Еще один семафор - mutex - обеспечивает взаимное исключение процессов.
var b_empty=n, b_full=0, mutex=1: semaphore; . . .
var full=0, empty=n; /*счетчики элементов и свободных мест . Producer||Consumer;
/* оператор || разрешает параллельное исполнение процессов Producer и Consumer */

Producer:
{repeat
...
производится очередной элемент данных
...
P(b_empty); /*число работающих процессов- производителей не должно превышать числа свободных мест в буфере*/
P(mutex);
...
добавляется вновь произведенный элемент данных в буфер
...
V(mutex);
V(b_full);
until false; };

Consumer:
{ repeat
P(b_full); /*число работающих процессов-потребителей не должно превышать числа произведенных элементов в буфере*/
P(mutex);
...
элемент данных забирается из буфера
...
V(mutex);
V(b_empty);
...
until false; }

Задача читатели-писатели
Рассмотрим более сложный пример решения задачи программирования взаимодействия множества процессов с использованием семафоров. Пусть выполняются n процессов, которые разделяют некоторую переменную программы. Часть процессов - писатели - только модифицируют разделяемый объект, другие - читатели - только считывают значение. Необходимо организовать корректное выполнение этой системы взаимодействующих процессов.
Прежде всего отметим, что процессы-читатели могут иметь одновременный доступ к разделяемому объекту, т.к. чтение не меняет значение объекта и, следовательно, процессы-читатели не могут влиять друг на друга. Для процессов-писателей следует организовать взаимное исключение при доступе к разделяемому объекту.

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

Эта модельная задача может реально интерпретироваться. Такая схема взаимодействий должна быть реализована, если нужно, к примеру, сделать Интернет-газету, которую любой читатель может читать, а репортеры (процессы-писатели) могут в любой момент, по мере поступления новой информации, её обновлять
Для программирования такого взаимодействия будут использованы 4 семафорные переменные Mutex_n_writers, Mutex_n_readers, NoWriter и NoReader и счетчики процессов-читателей n_readers и процессов-писателей n_writers.
[1] Программу разработал магистрант НГТУ А.Уразов

В программе не рассматриваются случаи аварийного завершения. Например, если последний процесс-читатель или последний процесс-писатель завершится аварийно и не откроет барьерный семафор (V(Mutex_n_writers) и/или V(Mutex_n_readers)), тогда система процессов, конечно, «зависнет».

Критические интервалы
Программируя межпроцессные взаимодействия с использованием семафоров легко допустить разнообразные неочевидные ошибки, в первую очередь ошибки временные, связанные с доступом к разделяемым данным.
В языках программирования вместо семафоров используются другие конструкции более высокого уровня. Одна из них - критические интервалы. Ее идея такова.
Вводится понятие разделяемой переменной, которая доступна из нескольких процессов.
Например: var x : shared real;
Разделяемые переменные доступны только внутри оператора region вида region x do S;

Только один процесс может исполнять оператор region с переменной x в качестве параметра. Таким образом, пока исполняется оператор S никакой другой процесс не может начать исполнение оператора region x. Понятно, что оператор region x реализуется программой
var x : semaphore;
P(x) S; … V(x)
Программировать с использованием оператора критического интервала несколько легче, однако в дедлок тоже легко попасть, например:
P1: region x do (region y do S1);
P2: region y do (region x do S2);
Очевидна возможность дедлока как следствие дозахвата ресурса, когда два процесса P1 и P2 одновременно начнут выполнять свои вложенные операторы region.

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

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

На практике следует комбинировать и тестирование и формальное доказательство правильности. Следует также обратить внимание на опасную кажущуюся правильность корректных, но не тотально корректных программ. Нередко такая программа долгое время нормально работает и обнаруживает ошибку в самый неподходящий момент. И большие сложные, особенно управляющие, программы отлаживаются иной раз десятилетиями и при этом успешно эксплуатируются.
Пусть заданы два множества натуральных чисел S и T. Сохраняя мощность множеств S и T необходимо собрать в S наименьшие элементы множества S∪T, а в Т - наибольшие.
Последовательный алгоритм и программа очевидны: множества S и T сливаются, затем слитое множество упорядочивается и вновь разделяются на на множества S’ и T’, удовлетворяющие условиям задачи.

Для параллельного асинхронного решения задачи используется следующий алгоритм.
-1.Определяются два параллельно протекающих процесса Small и Large.
-2.Процесс Small выбирает максимальный элемент в множестве S, а процесс Large параллельно (в то же самое время) находит минимальный элемент во множестве Т.
-3.Процессы Small и Large синхронизуются и обмениваются данными: наибольшее значения множества S пересылаются процессом Small процессу Large для включения в множество T, а наименьшее значения множества T пересылаются процессом Large процессу Small для включения в множество S.
-4.Далее циклически повторяются шаги 3 и 4.
-5.Программа останавливается, когда наибольший элемент в множестве S окажется меньше либо равен наименьшего элемента в множестве T.

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

Программа состоит из двух параллельных процессов,
P=[Small||Large].

Программу можно прокомментировать следующим образом. Определены два процесса Small и Large. Символ || разрешает параллельное исполнение процессов Small и Large, оператор * задает циклическое исполнение (итерацию), пока истинно условие циклов. Процессы связаны однонаправленными каналами α и β. По каналу α процесс Small передает данные в процесс Large, а данные из процесса Large передаются в процесс Small по канале β.

Оператор ! задает передачу данных (аналог оператора send), а оператор ? - их прием (аналог оператора receive). В частности, оператор α! mx в процессе Small задает передачу значения переменной mx в канал α, а оператор α?y в процессе Large определяет прием значения из канала α и присваивание этого значения переменной y.
В программе [Small||Large] одновременное выполнение оператора α!mx в процессе Small и оператора α?y в процессе Large (их выполнение синхронизуется, т.е., выполнение одного из них в одном из процессов задерживается до тех пор, пока другой оператор не начнет выполняться в другом процессе) имеет семантику “удаленного присваивания” у:=mx. Аналогична семантика взаимодействия по каналу β.

Обозначим S0 и T0 – начальные множества, а STerm и TTerm – заключительные их значения. При правильном завершении программы ожидается выполнение соотношений (в соответствии с начальными условиями задачи):
(С1). Объединение множеств не изменилось:
STerm ∪ TTerm = S0 ∪ T0;
(С2). Мощности множеств сохранились:
|STerm | = |S0|, |TTerm | = |T0|;
(C3). Каждый элемент STerm не больше любого элемента TTerm :
max(STerm) ≤ min(TTerm).

Частичная корректность этой программы состоит в том, что если множества S0 и T0 конечны и непусты, то после нормального завершения программы (т.е. когда каждый из процессов выходит на свой stop) свойства (С1), (С2) и (С3) выполняются. Тотальная корректность ее состоит в том, что если множества S0 и T0 конечны и непусты, то программа завершается правильно и свойства (С1), (С2) и (С3) непременно выполняются после этого завершения.
Оставляя в стороне формальные детали, весьма поучительно рассмотреть технологические приемы, приводящие к пониманию того, что программа не является тотально корректной.

4.2.3.Коммуникационно-замкнутые слои параллельной программы
Это понятие вводится для упрощения верификации (доказательства правильности) параллельных программ. Основная идея здесь - это разбиение каждого процесса Pi параллельной программы Р::=[P1|| ...||Pn] на последовательность его операторов: Pi=Qi,1;Qi,2;...Qi,k (k может быть выбрано одним и тем же для всех процессов, если допустить возможность использовать в качестве Qi,r пустой оператор). Таким образом, параллельная программа Р может быть представлена как:
P=[(Q1,1; Q 1,2;...; Q 1,k)||...||(Qi,1;Qi,2;...;Qi,k)|| ... ||(Qn,1;Qn,2;...;Qn,k)].
Эту программу можно изобразить матрицей (рис. 4.3)

Каждая i-я строка изображает процесс Pi как последовательность операторов: Pi=Qi,1;Qi,2;...Qi,k.
Параллельная программа Lj=[Q1,j||Q2,j||...||Qn,j] называется j-м слоем параллельной программы Р (j-й столбец матрицы).

Слой Lj называется коммуникационно-замкнутым, если при всех вычислениях Р взаимодействие процессов P1|| ...||Pn происходит только внутри этого слоя, или, иными словами, ни одна команда взаимодействия среди операторов Qr,j при всех выполнениях Р не будет синхронизироваться (сочетаться) с командами взаимодействия из операторов Qt,i при i≠j.
Тогда последовательность слоев L1;...;Lk представляет собой параллельную программу:
Р*= L1;...;Lk = [Q1,1||Q2,1||...||Qn,1];... ;[Q1,k||Q2,k||...||Qn,k],
В программе Р* все Lj исполняются последовательно в порядке перечисления, а операторы каждой Lj исполняются параллельно. Программа Р* называется безопасной, если и только если все ее слои коммуникационно-замкнуты.

Если программа Р* безопасна, то вместо верификацию всей параллельной программы Р можно проводить ее послойную верификацию, т.е., доказывать утверждение {p0}L1{p1},...,{pk-1}Lk{pk} вместо утверждения {p0}P{pk}. Здесь, как обычно, {s}P{q} обозначает утверждение, что программа P частично корректна по отношению к предусловию s и постусловию q (вход-выходные соотношения), при этом, если до начала исполнения программы P предикат s истинен, то после исполнения P предикат q тоже истинен.
Таким образом, если параллельную программу Р удается разбить на последовательность коммуникационно-замкнутых слоев, то доказательство ее (частичной) корректности сводится к последовательному доказательству вход-выходных соотношений для каждого слоя. Это существенно упрощает анализ корректности параллельной программы.

Рис. 4.4.

Процессы Small и Large разбиваются на коммуникационно-замкнутые слои совершенно естественно. Разбиение приведено на рис. 4.4.
На рисунке показаны только “синхронизационные скелеты” параллельных процессов. В первый слой входят операторы до цикла, во второй слой - операторы внутри цикла, третий слой составляет оператор stop после выхода из цикла. Процесс правильно завершается, если он заканчивает вычисления в заключительном состоянии: процесс Small в состоянии ЕS , а процесс Large в состоянии EL. В общем случае процессы могут:
а) оба завершиться нормально,
б) оба не завершатся,
в)один завершится, а другой нет, например, при невозможности выполнить операцию синхронного взаимодействия.
Условия BS и BL определяют условия окончания циклов в процессах; они равны соответственно mx ≤ x и mn ≥ y.

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

В когерентной программе невозможна ситуация, когда в одном процессе выполняется оператор α! mx, а процесс-партнер не может выйти на исполнение оператора α?y.
Если параллельная программа Р::=[P1||...||Pn] разбита на коммуникационно-замкнутые слои Pi= Qi,1;Qi,2;...Qi,k, то требование когерентности состоит не только в том, что при всех вычислениях Р ни одна команда взаимодействия среди операторов Qr,j при всех выполнениях Р не будет синхронизироваться (сочетаться) с командами взаимодействия из операторов Qt,i при i≠j, но и в том, что каждая такая команда взаимодействия обязательно будет сочетаться с некоторой командой взаимодействия из операторов того же самого слоя. Для параллельной программы P=[Small || Large] такая синхронизация показана на рис. 4.5.

Очевидно, что требование когерентности для этой программы выполняется тогда и только тогда, когда условия прекращения циклов в программах Small и Large тождественны при всех прохождениях циклов.
Некогерентность, с другой стороны, ведет к блокировке этой программы, т.е., к возникновению ситуации, когда один из процессов выходит из цикла и переходит в заключительное состояние, а другой не выходит из своего цикла и “зависает” на операции синхронного взаимодействия внутри цикла, бесконечно ожидая партнера.

Рис. 4.5.

Таким образом, условие BS ≡ BL≡ И, или, что то же, mx ≤ x ≡ mn ≥ y при каждой проверке условий циклов в обоих программах, является необходимым условием тотальной корректности этой параллельной программы.

4.2.5.Анализ программы разделения множеств
Для анализа программы используем “истории” взаимодействий. Вводятся вспомогательные переменные, которые хранят истории взаимодействия по каждому каналу программы.
Историческая переменная - это просто массив значений, последовательно переданных по соответствующему каналу. Пусть hα и hβ такие исторические переменные для каналов α и β соответственно, тогда компонент hα[k] содержит k-е значение, посланное по каналу α при выполнении операции α!е.

Проведем анализ первого слоя :

Для того, чтобы процессы QSmall,1 и QLarge,1 завершились, необходимо и достаточно, чтобы множество S содержало хотя бы один элемент, т.е. |S|>0. По завершении каждого из этих параллельных процессов первого слоя будут справедливы следующие соотношения:
Эти соотношения просто описывают, что было сделано при исполнении операторов первого слоя.

Рассмотрим теперь второй слой:
Перед i-м выполнением каждого цикла для процессов QSmall,2 и QLarge,2 истинны следующие инварианты, что можно проверить непосредственно (где аi -значение переменной а перед i-ым выполнением цикла):

Как уже говорилось, требование когерентности в этой программе соответствует требованию общезначимости формулы mxi ≤ xi ≡ mni ≥ yi. При некоторых значениях исходных множеств S и T она нарушается. Возможны два случая некогерентности:
при этом процесс Small завершается, а процесс Large продолжает выполнять цикл, что приводит к его блокировке;
при этом процесс Large завершается, а процесс Small продолжает выполнять цикл и блокируется, бесконечно ожидая взаимодействия с процессом Large.

Учитывая, что min(Ti) ≥ min(Ti-1) и max(Si) ≤ max(Si-1), условия некорректного поведения параллельной программы разделения множеств можно записать проще:

Поясним полученный результат. Исследуемая параллельная программа разделения множеств имеет целью собрать все минимальные элементы объединения двух множеств S и T в множестве S, а максимальные элементы S∪T - в множестве T, причем мощности множеств не должны измениться. Упорядочим элементы исходных множеств: множества S по убыванию, а множества Т по возрастанию. На рис. 4.6а. показано, что процесс Small, работая на множестве S, пересылает его максимальные элементы в множество Т, а процесс Large, работая на множестве Т, пересылает его минимальные элементы в множество S.

Рис. 4.6.
Полученные выше условия некорректного поведения программы определены для (i-1)-го и i-го максимальных значений множества S и для (i-1)-го и i-го минимальных значений множества Т, (i =1,2, ...). Эти условия представлены диаграммами на рис. 4.6.б) и 4.6.в).

Иными словами, если между упорядоченными по убыванию элементами множества S и упорядоченными по возрастанию элементами множества Т на одном и том же расстоянии от начала выполнится одно из отношений рис. 4.6,б) или рис. 4.6,в), то исследуемая программа будет работать некорректно: она входит в дедлок.