Принципы реализации формальной модели взаимодействующих
последовательных процессов
В работе Хоара [1] рассматриваются вопросы реализации рассмат-
риваемой формальной модели на языке программирования ЛИСП. В
основе такой реализации лежит функциональный подход. Согласно
этому подходу, каждый процесс представляется в виде функции, аргу-
менты которой
− события из алфавита этого процесса, а результат
функции
− другая функция, определяющая последующее поведение
143
процесса. Для описания процесса, определяемого рекурсивно, исполь-
зуется рекурсивный вызов функции, где в качестве аргумента, описы-
вающего дальнейшее поведение процесса, используется сама эта
функция. Операции последовательной и параллельной композиции
также определяются как функции, аргументами которой являются объ-
единяемые процессы. ЛИСП-реализация модели позволяет проводить
доказательство беступиковости сложного составного процесса, про-
верку соответствия модели требуемой спецификации. Однако такую
реализацию очень трудно модифицировать в направлении, позволяю-
щем учесть фактор времени.
В основе предлагаемой программной реализации формальной мо-
дели лежит объектно-ориентированный подход, который прямо соот-
носится с основными понятиями CSP теории. Основной единицей мо-
делирующей программы является объект событие. Процесс
− это
также объект, который содержит упорядоченный список событий, в
которых он участвует. Рассмотрим основные моменты предлагаемого
алгоритма моделирования CSP-алгебры. Функционирование возможно
в двух вариантах: верификация процесса на предмет отсутствия тупи-
ков и моделирование процесса обработки со сбором статистики време-
ни исполнения.
В режиме верификации процесс, получая управление, последова-
тельно запускает собственные события. Простое событие устанавлива-
ет следующее в списке событие в качестве текущего и передает управ-
ление процессу. Процесс проверяет свое состояние и, если он не при-
остановлен, запускает текущее событие, если процесс приостановлен,
то управление передается на верхний уровень. При исследовании
только одного изолированного процесса моделирование на этом за-
канчивается. В случае параллельной композиции нескольких процес-
сов на верхнем уровне формируется список процессов, исполняемых
параллельно. При возврате управления на этот уровень запускается
любой следующий процесс, готовый к исполнению. Если готовых к
исполнению процессов нет, причем процессы не завершили свою ра-
боту (состояние «Завершен» отлично от состояния «Приостановлен»),
значит система пришла в тупиковое состояние
− дедлок. Состояние
процесса изменяют события из класса взаимодействий. Событие-
взаимодействие присутствует во всех содержащих его процессах, при-
чем, происходит оно в них одновременно. Если какой либо процесс
144
первым переходит к такому событию, то он приостанавливается до тех
пор, пока остальные, участвующие во взаимодействии процессы не
дойдут до момента взаимодействия. Как только все процессы, участ-
вующие во взаимодействии, доживут до него, событие происходит в
каждом процессе, т.е. состояние «Приостановлен» сбрасывается, и
последующее событие устанавливается в качестве текущего во всех
процессах, а управление передается любому из взаимодействующих
процессов, который и выполняется до наступления следующего собы-
тия-взаимодействия, либо до своего завершения. Последнее событие
из списка процесса устанавливает состояние «Завершен» и передает
управление на верхний уровень. Далее опять запускается любой сле-
дующий процесс, готовый к исполнению. Верификация завершается
успешно, если все процессы, составляющие исследуемую потоковую
сеть, перешли в состояние «Завершен».
В режиме моделирования берется за основу квантовая модель вре-
мени, то есть наименьшим промежутком времени, которым оперирует
моделирующая программа, является квант. Все события, происходя-
щие в системе, имеют длительность, кратную выбранному кванту вре-
мени. В объект событие добавляется параметр, определяющий коли-
чество квантов времени, потребляемых событием до своего заверше-
ния. Процесс моделирования несколько отличен от верификации. На
верхнем уровне формируется циклический список процессов, состав-
ляющих исследуемую сеть. Затем программа начинает последователь-
но генерировать временные кванты и передавать их очередному про-
цессу. Процесс получает один квант и либо поглощает его, либо воз-
вращает неиспользованным, в последнем случае этот неиспользован-
ный квант передается для обработки следующему по списку процессу.
Если процесс использовал выделенный ему квант времени, указатель в
очереди смещается на следующий процесс, которому и будет передан
очередной квант для обработки. На уровне процесса обработка кванта
выполняется следующим образом: если процесс приостановлен, то
квант возвращается неиспользованным, если процесс находится в ра-
бочем состоянии, то квант передается для обработки в текущее собы-
тие процесса. Событие потребляет необходимое для завершения коли-
чество квантов и при обработке последнего кванта устанавливает сле-
дующее в списке процесса событие в качестве текущего. Событие-
взаимодействие представляется в виде двух событий: собственно со-
145
бытия-взаимодействия, обрабатываемого аналогично режиму верифи-
кации, и простого события, следующего за взаимодействием и опреде-
ляющего его длительность. После обработки последнего события про-
цесс удаляется из циклического списка, описывающего сеть. На каж-
дом шаге, при генерации очередного кванта проверяется количество
приостановленных процессов, если это количество равно числу про-
цессов в списке, то значит сеть находится в заблокированном состоя-
нии. Когда список становится пустым, процесс моделирования завер-
шается, количество сгенерированных квантов определяет общее время
обработки. В процессе моделирования собирается информация о вре-
мени выполнения каждого процесса и его простоя, времени, которое
потребляют выбранные события, и т.д.
Помимо простых событий и событий-взаимодействий для модели-
рования процессов в системе используются события, реализующие
оператор присваивания, условный оператор и цикл. Предполагается,
что эти служебные события не потребляют временной квант. Услов-
ный оператор и цикл просто переустанавливают указатель текущего
события в соответствии со значением логической функции. Оператор
присваивания изменяет значение некоторой переменной процесса и
устанавливает следующее событие как текущее. Если необходимо
учесть время выполнения таких конструкций, то в список событий
процесса за служебным событием (или перед ним) вставляется простое
событие соответствующей длительности.
Данная квантовая модель естественным образом обобщается на
случай выполнения потоковой сети на нескольких процессорах. При
этом список процессов, составляющих такую распределенную сеть,
подразделяется на несколько подсписков, соответствующих конкрет-
ному компьютеру. Внутри каждого подсписка независимо формирует-
ся собственный квант времени, который потребляют составляющие
его процессы.
Достарыңызбен бөлісу: |