Процессы

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

ОПРЕДЕЛЕНИЕ-ПРОЦЕССА ::=

process ИМЯ-ПРОЦЕССА [( [ОПИСАНИЯ-АРГУМЕНТОВ] :

ОПИСАНИЯ-РЕЗУЛЬТАТОВ-ГИПЕРФУНКЦИИ )]

{ ТЕЛО-ПРОЦЕССА [МЕТКА :]}

[spec ВНЕШНЯЯ-СПЕЦИФИКАЦИЯ-ПРОЦЕССА]

ИМЯ-ПРОЦЕССА ::= ИДЕНТИФИКАТОР

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

ВНЕШНЯЯ-СПЕЦИФИКАЦИЯ-ПРОЦЕССА описывает эффект функционирования процесса на внешнее окружение, в рамках которого существует процесс. В общем случае этот эффект невозможно выразить с помощью предусловия и постусловия. В качестве языков внешней спецификации процессов ранее использовались язык алгебры процессов CCS [8] Р. Милнера и язык спецификации TLA+ [9] Л. Лампорта. Язык внешней спецификации в данном документе не фиксируется. Наиболее адекватным и проработанным представляется язык SAL [10].

ТЕЛО-ПРОЦЕССА ::= ОПИСАНИЕ-ПЕРЕМЕННЫХ [; ТЕЛО-ПРОЦЕССА] |

ВОЗМОЖНО-ПОМЕЧЕННЫЙ-ОПЕРАТОР [; ТЕЛО-ПРОЦЕССА]

ВОЗМОЖНО-ПОМЕЧЕННЫЙ-ОПЕРАТОР ::= [МЕТКА :] ОПЕРАТОР

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

Языковые конструкции ОПЕРАТОР, ПЕРВИЧНОЕ-ВЫРАЖЕНИЕ и ИДЕНТИФИКАЦИЯ-ПРЕДИКАТА, определенные выше, имеют доопределение для процессов.

ИДЕНТИФИКАЦИЯ-ПРЕДИКАТА ::= ... | [ОБЪЕКТ-КЛАССА .] ИМЯ-ПРЕДИКАТА

ОБЪЕКТ-КЛАССА ::= ПЕРВИЧНОЕ-ВЫРАЖЕНИЕ

Конструкция ИДЕНТИФИКАЦИЯ-ПРЕДИКАТА используется в вызове предиката для указания вызываемого предиката.

ОПЕРАТОР-РАБОТЫ-С-ПРОЦЕССАМИ ::=

ВЫЗОВ-ПРОЦЕССА | ЗАПУСК-НЕЗАВИСИМОГО-ПРОЦЕССА |

ПАРАЛЛЕЛЬНАЯ-КОМПОЗИЦИЯ-ПРОЦЕССОВ | ПРИЕМ-СООБЩЕНИЯ |

ПОСЫЛКА-СООБЩЕНИЯ | ЗАЩИЩЕННЫЙ-ОПЕРАТОР | ОПЕРАТОР-ПЕРЕХОДА

ВЫЗОВ-ПРОЦЕССА ::=

[ ОБЪЕКТ-КЛАССА . ] ИМЯ-ПРОЦЕССА ( [АРГУМЕНТЫ] (: РЕЗУЛЬТАТЫ-ВЕТВИ)*] )

ОБЪЕКТ-КЛАССА ::= ПЕРВИЧНОЕ-ВЫРАЖЕНИЕ

Процесс, запускаемый на исполнение ВЫЗОВОМ-ПРОЦЕССА, должен иметь соответствующее определение процесса. Если определение процесса принадлежит некоторому классу, то вызов процесса реализуется через ОБЪЕКТ-КЛАССА.

ПАРАЛЛЕЛЬНАЯ-КОМПОЗИЦИЯ-ПРОЦЕССОВ ::= ПАРАЛЛЕЛЬНЫЙ-ОПЕРАТОР

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

ОПИСАНИЕ-СООБЩЕНИЯ ::= message ИМЯ-СООБЩЕНИЯ [( СПИСОК-ТИПОВ )] |

queue ИМЯ-СООБЩЕНИЯ [( СПИСОК-ТИПОВ )]

ИМЯ-СООБЩЕНИЯ ::= ИДЕНТИФИКАТОР

СПИСОК-ТИПОВ ::= ИЗОБРАЖЕНИЕ-ТИПА [, СПИСОК-ТИПОВ]

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

ПОСЫЛКА-СООБЩЕНИЯ ::=

ИМЯ-ПРОЦЕССА> ! ИМЯ-СООБЩЕНИЯ [( СПИСОК-ВЫРАЖЕНИЙ )] |

ИМЯ-СООБЩЕНИЯ ! [( СПИСОК-ВЫРАЖЕНИЙ )]

Оператор посылает сообщение с набором значений, вычисленных СПИСКОМ-ВЫРАЖЕНИЙ. Если сообщение определено описанием message, то выполнение оператора не будет завершено до тех пор, пока это сообщение не будет принято получателем. Для сообщения, определенного описанием queue, оператор вставляет сообщение в конец очереди посланных сообщений и завершает свою работу.

ПРИЕМ-СООБЩЕНИЯ ::= receive СООБЩЕНИЕ |

ПРИЕМ-СООБЩЕНИЯ-ОБЩЕГО-ВИДА

СООБЩЕНИЕ ::= ИМЯ-СООБЩЕНИЯ [(СПИСОК-ПЕРЕМЕННЫХ )]

Допустим, что процесс, исполняющий оператор receive СООБЩЕНИЕ, получил сообщение с именем, указанным в операторе. Исполнение оператора заключается в присваивании перечисленным переменным соответствующих значений, поставляемых сообщением. Если исполняемый процесс не получил сообщения с указанным именем, то исполнение оператора приостанавливается (блокируется) до поступления требуемого сообщения.

ПРИЕМ-СООБЩЕНИЯ-ОБЩЕГО-ВИДА ::= receive { СООБЩЕНИЕ : ОПЕРАТОР

( or СООБЩЕНИЕ : ОПЕРАТОР )*

[ after ВРЕМЯ-ОЖИДАНИЯ : ОПЕРАТОР ]

}

ВРЕМЯ-ОЖИДАНИЯ ::= ВЫРАЖЕНИЕ

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

ПЕРВИЧНОЕ-ВЫРАЖЕНИЕ ::= ... | СООБЩЕНИЕ

Конструкция СООБЩЕНИЕ в любой позиции логического выражения трактуется как неблокирующий прием сообщений. Исполнение конструкции осуществляется следующим образом. В очереди пришедших сообщений исполняемого процесса ищется сообщение с именем, указанным в конструкции СООБЩЕНИЕ. Если сообщение обнаружено, оно вычеркивается из очереди. При этом значения параметров присваиваются соответствующим переменным, перечисленным в круглых скобках. Результатом исполнения конструкции СООБЩЕНИЕ является значение true. Если требуемое сообщение не обнаружено в очереди, исполнение конструкции СООБЩЕНИЕ завершается значением false.

Динамическое создание нового процесса и его запуск реализуется через объект класса. Объект (или значение) типа "класс" является структурой, составленной из полей класса. Описание класса определяется следующим образом:

ОПРЕДЕЛЕНИЕ-КЛАССА ::=

class ИМЯ-КЛАССА [extends ИМЯ-СУПЕРКЛАССА] { ТЕЛО-КЛАССА }

ИМЯ-КЛАССА ::= ИДЕНТИФИКАТОР

ТЕЛО-КЛАССА ::= ОПИСАНИЕ-КЛАССА [; ТЕЛО-КЛАССА]

ОПИСАНИЕ-КЛАССА ::=

ОПИСАНИЕ-ТИПА | ОПИСАНИЕ-ПЕРЕМЕННЫХ | ОПИСАНИЕ-СООБЩЕНИЯ |

ОПРЕДЕЛЕНИЕ-ПРОЦЕССА | ОПРЕДЕЛЕНИЕ-ПРЕДИКАТА |

ОПИСАНИЕ-КОНСТРУКТОРА-КЛАССА

ОПИСАНИЕ-КОНСТРУКТОРА-КЛАССА ::=

ИМЯ-КЛАССА ([<ОПИСАНИЯ-АРГУМЕНТОВ>]) { ТЕЛО-КОНСТРУКТОРА }

ТЕЛО-КОНСТРУКТОРА ::= [ ТЕЛО-БЛОКА ]

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

Отметим, что классы не интегрированы с системой типов языка P.

ПЕРВИЧНОЕ-ВЫРАЖЕНИЕ ::= ... | СОЗДАНИЕ-ОБЪЕКТА

СОЗДАНИЕ-ОБЪЕКТА ::= new ИМЯ-КЛАССА ( [<АРГУМЕНТЫ>] )

Операция СОЗДАНИЯ-ОБЪЕКТА реализует вызов конструктора, параметры которого соответствуют списку аргументов. Результатом операции является новый объект (значение) типа ИМЯ-КЛАССА. При исполнении конструктора создается объект - структура, полями которой являются переменные, описанные в теле класса. Для созданного объекта исполняются ОПИСАНИЯ-ПЕРЕМЕННЫХ, находящиеся в теле класса и содержащие инициализацию переменных. Далее исполняется тело конструктора.

Если для операции new ИМЯ-КЛАССА( ) нет соответствующего конструктора с пустым списком аргументов, то такой конструктор считается определенным и его тело пусто.

ИМЯ-СУПЕРКЛАССА ::= ИМЯ-КЛАССА

При наличии подконструкции extends ИМЯ-СУПЕРКЛАССА определяемый класс является расширением суперкласса, представленного описателем extends. Структура, создаваемая для определяемого класса, содержит поля суперкласса, за которыми следуют поля определяемого класса. Конструктор класса содержит явный или неявный вызов соответствующего конструктора для суперкласса.

ПЕРВИЧНОЕ-ВЫРАЖЕНИЕ ::= ... | ДИНАМИЧЕСКОЕ-СОЗДАНИЕ-ПРОЦЕССА

 

ДИНАМИЧЕСКОЕ-СОЗДАНИЕ-ПРОЦЕССА ::=

new ИМЯ-ПРОЦЕССА ( [<АРГУМЕНТЫ>] )

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

ЗАЩИЩЕННЫЙ-ОПЕРАТОР ::=

with СПИСОК-РАЗДЕЛЯЕМЫХ-ПЕРЕМЕННЫХ { ОПЕРАТОР }

СПИСОК-РАЗДЕЛЯЕМЫХ-ПЕРЕМЕННЫХ ::= СПИСОК-ПЕРЕМЕННЫХ

Взаимодействие между параллельными процессами возможно через разделяемые переменные, доступные для нескольких процессов и являющиеся глобальными по отношению к ним. Доступ к разделяемым переменным разрешен только внутри защищенного оператора. При исполнении ОПЕРАТОРА доступ к перечисленным разделяемым переменным блокируется. Блокировка снимается при завершении исполнения ОПЕРАТОРА. Если при попытке исполнить ЗАЩИЩЕННЫЙ-ОПЕРАТОР одна из разделяемых переменных оказалась блокирована другим процессом, исполнение текущего процесса, исполняющего ЗАЩИЩЕННЫЙ-ОПЕРАТОР, приостанавливается до момента снятия блокировки с разделяемой переменной.