Теория процессов
 Скачать 1.62 Mb.
|
|
get_and_work? put? Отметим, что объект “молоток” и процесс “молоток” - это разные понятия. Функционирование мастерской определяется при помощи сле- дующего процесса J ob_Shop: J ob_Shop = (J obber | J obber | M allet) \ L где L = {get_and_work, put}. 144 Потоковый граф процесса J ob_Shop имеет следующий вид. ' & $ % ' & $ % ' & $ % J obber M allet J obber u u u u e e e e u u @ @ @ @ @ @ I @ @ R get_and_work get_and_work put put in in out out Введем теперь понятие “абстрактного рабочего”, про которого известно, что он циклически • принимает материал, и • выдает готовые изделия но ничего неизвестно о подробностях процесса его работы. Поведение “абстрактного рабочего” мы зададим при помощи следующего процесса Abs_J obber: Abs_J obber Doing - in? out! Поведение “абстрактной мастерской” мы зададим при помо- щи следующего процесса Abs_J ob_Shop: Abs_J ob_Shop = Abs_J obber | Abs_J obber “Абстрактную мастерскую” мы будем использовать как спе- цификацию мастерской. Процесс “абстрактная мастерская” пре- дставляет поведение мастерской без учета деталей ее реализа- ции. 145 Докажем соответствие мастерской ее спецификации, то есть наличие наблюдаемой конгруэнции J ob_Shop + ≈ Abs_Job_Shop (6.2) Процесс Abs_J ob_Shop является параллельной композицией двух процессов Abs_J obber. В целях предотвращения коллизии в обозначениях, мы выберем различные идентификаторы для обо- значения состояний этих процессов. Пусть, например, эти про- цессы имеют вид A i D i - in? out! где i = 1, 2. Параллельная композиция этих процессов имеет вид A 1 , A 2 D 1 , A 2 D 1 , D 2 A 1 , D 2 - in? out! - in? out! ? 6 in? out! ? 6 in? out! Применяя к данному процессу процедуру минимизации отно- сительно наблюдаемой эквивалентности, мы получим процесс - - in? out! in? out! (6.3) Процесс J ob_Shop имеет 4 · 4 · 2 = 32 состояния, и мы не приводим его здесь ввиду его большой громоздкости. Если ми- нимизировать этот процесс относительно наблюдаемой эквива- лентности, то получится процесс, изоморфный процессу (6.3). 146 Это означает, что имеет место соотношение J ob_Shop ≈ Abs_J ob_Shop (6.4) Поскольку из начальных состояний процессов J ob_Shop и Abs_J ob_Shop не выходит рёбер с меткой τ , то отсюда и из (6.4) следует искомое соотношение (6.2). 6.3 Неконфликтное использование ресу- рса Предположим, что имеется некоторая фирма, сотрудники кото- рой объединены в несколько групп. В здании, где работает фирма, выделена одна комната, кото- рую каждая из групп может использовать для проведения своих рабочих совещаний. Предположим, что необходимо обеспечить неконфликтное ис- пользование этой комнаты группами. Это означает, что когда од- на из групп проводит в комнате совещание, другой группе долж- но быть запрещено проводить своё совещание в этой комнате. Для решения этой задачи создаётся специальный процесс – диспетчер. Если какая-либо из групп хочет провести совещание в этой комнате, она должна послать диспетчеру заявку на предостав- ление ей права пользования комнатой для проведения этого со- вещания. Когда диспетчер разрешает какой-либо группе использовать комнату, он посылает ей уведомление об этом. Окончив совещание, группа должна сообщить об этом дис- петчеру, чтобы диспетчер знал, что комната стала свободной и доступна для других групп. Рассмотрим описание работы указанной системы при помощи теории процессов. Пусть число групп равно n (n ≥ 2). 147 Диспетчер мы опишем как процесс с именем D, графовое представление которого содержит для каждого i = 1, . . . , n под- граф D d i1 d i2 ? - @ @ @ @ @ @ @ @ @ I req i ? acq i ! rel i ? т.е. D ∼ n X i=1 req i ?. acq i !. rel i ?. D Действия, входящие в Act(D), имеют следующий смысл: • req i ? – получение заявки от i-й группы • acq i ! – уведомление i-й группы о том, что она имеет право пользоваться комнатой • rel i ? – получение сообщения от i-й группы об освобождении ею комнаты. Опишем теперь поведение каждой группы. (Мы будем описывать только взаимодействие групп с диспет- чером и с комнатой, и не будем касаться прочих их функций). Мы будем представлять • начало проведения совещания в комнате действием start!, и • окончание совещания - действием f inish!. 148 Поведение i-й группы мы опишем в виде процесса G i , кото- рый имеет следующее графовое представление: g i0 g i1 g i2 g i3 g i4 ? - 6 6 req i ! acq i ? start i ! f inish i ! rel i ! т.е. G i ∼ req i !. acq i ?. start!. f inish!. rel i !. G i Совместное поведение диспетчера и групп можно описать сле- дующим процессом: Sys = (D | G 1 | . . . | G n ) \ L где L = {req i , acq i , rel i | i = 1, . . . , n}. Потоковый граф системы, состоящей из диспетчера и групп для n = 2 показан на рисунке ' & $ % ' & $ % ' & $ % G 1 D G 2 u e u u e u e u e e u e u u u u - - - rel 1 acq 1 req 1 rel 2 acq 2 req 2 start start f inish f inish Покажем теперь, что алгоритмы работы диспетчера и групп действительно обеспечивают неконфликтный режим использо- вания комнаты, который заключается в том, что после начала проведения совещания в комнате какой-либо группой (то есть после выполнения этой группой действия start!) никакая другая 149 группа не может начать проводить в этой комнате своё сове- щание (т.е. тоже выполнить действие start!), до тех пор первая группа не закончит своё совещание (т.е. пока не будет выполнено действие f inish!). Определим процесс Spec следующим образом: - start! f inish! т.е. Spec ∼ start!. f inish!. Spec. Наличие неконфликтного режима использования комнаты эк- вивалентно истинности соотношения Sys ≈ Spec (6.5) Это соотношение можно рассматривать как требование к систе- ме, состоящей из диспетчера и групп. Докажем соотношение (6.5). Преобразуем процесс Sys, применив несколько раз теорему о разложении: Sys ∼ ∼ n P i=1 τ. acq i !. rel i ?. D | G 1 | . . . . . . | acq i ?. start!. f inish!. rel i !. G i | . . . . . . | G n \ L ∼ ∼ n P i=1 τ.τ. rel i ?. D | G 1 | . . . . . . | start!. f inish!. rel i !. G i | . . . . . . | G n \ L ∼ ∼ n P i=1 τ.τ.start!. rel i ?. D | G 1 | . . . . . . | f inish!. rel i !. G i | . . . . . . | G n \ L ∼ ∼ n P i=1 τ.τ.start!. f inish!. rel i ?. D | G 1 | . . . . . . | rel i !. G i | . . . . . . | G n \ L ∼ ∼ n P i=1 τ.τ.start!. f inish!. τ. D | G 1 | . . . . . . | G i | . . . . . . | G n \ L | {z } Sys = = n P i=1 τ.τ.start!. f inish!. τ.Sys 150 Воспользовавшись тождествами P + P ∼ P и α.τ.P + ≈ α.P получаем отсюда, что Sys + ≈ τ.start!. f inish!. Sys Рассмотрим теперь уравнение X = τ.start!. f inish!. X (6.6) Согласно теореме 33 из параграфа 5.8, решение этого урав- нения с точностью до + ≈ единственно. Как было показано выше, процесс Sys является решением уравнения (6.6) с точностью до + ≈. Процесс τ.Spec тоже является решением уравнения (6.6) с точностью до + ≈, так как τ.Spec ∼ τ.start!. f inish!. Spec + ≈ + ≈ τ.start!. f inish!. (τ.Spec) Следовательно, имеет место соотношение Sys + ≈ τ.Spec из которого следует (6.5). 6.4 Планировщик Предположим, что имеется n процессов P 1 , . . . , P n (6.7) и для каждого i = 1, . . . , n среди действий, которые может вы- полнить P i , есть два служебных действия: • действие α i ?, которое представляет собой сигнал P i начинает работу (6.8) 151 • действие β i ?, которое представляет собой сигнал P i заканчивает работу (6.9) Мы предполагаем, что все имена α 1 , . . . , α n , β 1 , . . . , β n (6.10) различны, и для каждого i = 1, . . . , n имена из names(Act(P i )) \ {α i , β i } не совпадают ни с одним именем из (6.10). Обозначим множество имён из (6.10) символом L. Для каждого i = 1, . . . , n действия из множества Act(P i ) \ {α i ?, β i ?} называются собственными действиями процесса P i Произвольная трасса каждого процесса P i может содержать действия α i ? и β i ? в любом количестве и в любом порядке. Мы хотели бы создать новый процесс P , в котором все про- цессы P 1 , . . ., P n работали бы совместно, причём эта совместная работа должна подчиняться определённому режиму. Процесс P должен иметь вид P = (P 1 | . . . | P n | Sch) \ L где процесс Sch называется планировщиком и предназначен для задания требуемого режима работы процессов P 1 , . . ., P n Процесс Sch должен выполнять только действия из множества {α 1 !, . . . , α n !, β 1 !, . . . , β n !} (6.11) В силу определения процесса P , для каждого i = 1, . . . , n • каждое исполнение процессом P i ∈ (6.7) действия α i ? или β i ? в составе процесса P может произойти только одновре- менно с исполнением комплементарного действия процес- сом Sch, и 152 • исполнение этих действий будет невидимо за пределами процесса P . Говоря неформально, каждый процесс P i , работающий в со- ставе процесса P , может начать или закончить какой-либо сеанс своей работы тогда и только тогда, когда планировщик Sch раз- решит ему это сделать. Режим, которому должна подчиняться работа процессов P 1 , . . ., P n , заключается в следующих двух условиях. 1. Для каждого i = 1, . . . , n произвольная трасса процесса P i , работающего в составе процесса P , должна иметь вид α i ? . . . β i ? . . . α i ? . . . β i ? . . . где точки изображают собственные действия процесса P i , т.е. функционирование процесса P i должно представлять собой последовательность сеансов вида α i ? . . . β i ? . . . где каждый сеанс • начинается с сигнала α i ? о начале сеанса • далее выполняются некоторые собственные действия процесса P i • затем производится сигнал β i ? о завершении сеанса, • после чего процесс P i может производить некоторые собственные действия (например, связанные с подго- товкой к следующему сеансу). 2. Процессы P i должны начинать новые сеансы только по оче- реди в циклическом порядке, т.е. • сначала может начать свой первый сеанс только про- цесс P 1 • потом может начать свой первый сеанс процесс P 2 • . . . 153 • затем может начать свой первый сеанс процесс P n • после этого может начать свой второй сеанс процесс P 1 • затем может начать свой второй сеанс процесс P 2 • и т.д. Отметим, что мы не требуем, чтобы каждый процесс P i получал разрешение начать свой k-й сеанс только после того, как преды- дущий процесс P i−1 завершит свой k-й сеанс. Однако мы требуем, чтобы каждый процесс P i получал разрешение начать новый се- анс, только если он выполнил действие β i ?, сигнализирующее о завершении своего предыдущего сеанса. Исполнение собственных действий процессами P i может про- изводиться в произвольном порядке, в том числе допускается и взаимодействие между этими процессами во время их работы в составе процесса P . Описанный режим можно равносильным образом выразить в виде следующих двух условий на произвольную трассу tr ∈ T r(Sch) В формулировке этих условий мы будем использовать следую- щее обозначение: если tr ∈ T r(Sch) и M ⊆ Act то знакосочетание tr | M обозначает последовательность действий, получаемую из tr удалением всех действий, не принадлежащих M . Условия, выражающие описанный выше режим, имеют сле- дующий вид: ∀ tr ∈ T r(Sch), ∀ i = 1, . . . , n tr | {α i ,β i } = (α i ! β i ! α i ! β i ! α i ! β i ! . . .) (6.12) и ∀ tr ∈ T r(Sch) tr | {α 1 ,...,α n } = (α 1 ! . . . α n ! α 1 ! . . . α n ! . . .) (6.13) 154 Данные условия можно выразить равносильным образом в виде условия наличия наблюдаемой эквивалентности между неко- торыми процессами. Чтобы определить эти процессы, мы введём вспомогательные обозначения. 1. Пусть a 1 . . . a n – некоторая последовательность действий из Act. Тогда знакосочетание (a 1 . . . a n ) ∗ обозначает процесс, графовое представление которого име- ет следующий вид: - - - ? a n a 1 a 2 a n−1 2. Пусть заданы • некоторый процесс P , и • некоторое множество действий {a 1 , . . . , a k } ⊆ Act \ {τ } (6.14) Знакосочетание hide (P, a 1 , . . . , a k ) (6.15) обозначает процесс ( P | ( a 1 ) ∗ | . . . | ( a k ) ∗ ) \ names({a 1 , . . . , a k }) Процесс (6.15) можно рассматривать как процесс, получаемый из P заменой меток переходов: все метки переходов в P , принад- лежащие множеству (6.14), заменяются на τ . Используя введённые обозначения, условие (6.12) можно вы- разить следующим образом: для каждого i = 1, . . . n hide Sch, α 1 !, . . . , α i−1 !, α i+1 !, . . . , α n ! β 1 !, . . . , β i−1 !, β i+1 !, . . . , β n ! ! ≈ ≈ (α i !. β i !) ∗ (6.16) 155 Условие (6.13) можно выразить следующим образом: hide (Sch, β 1 !, . . . , β n !) ≈ (α 1 !. . . . α n !) ∗ (6.17) Нетрудно заметить, что существует несколько планировщи- ков, удовлетворяющих данным условиям. Например, данным усло- виям удовлетворяют следующие планировщики: • Sch = (α 1 ! β 1 ! . . . α n ! β n !) ∗ • Sch = (α 1 ! . . . α n ! β 1 ! . . . β n !) ∗ Однако такие планировщики налагают слишком жёсткие огра- ничения на работу процессов P 1 , . . . , P n Нам хотелось бы, чтобы планировщик допускал максималь- ную свободу в поведении процессов P 1 , . . . , P n в составе процесса P . Это одначает, что если в какой-либо момент времени • какой-либо процесс P i имеет намерение выполнить действие a ∈ {α i ?, β i ?}, и • это намерение процесса P i не противоречит описанному вы- ше режиму то планировщик не должен отказывать процессу P i в возмож- ности выполнить это действие в текущий момент времени, т.е. среди действий планировщика, которые он может выполнить в текущий момент времени, должно присутствовать действие a (не факт, что именно это действие будет выполнено в текущий мо- мент времени, но среди возможных действий оно должно при- сутствовать). Сформулированное выше неформальное описание максима- льной свободы в поведении планировщика можно формально уточнить следующим образом: • каждому состоянию s планировщика можно сопоставить метку label(s), имеющую вид пары (i, X) где – i ∈ {1, . . . , n}, i = номер того процесса, который имеет право начать очередной сеанс в текущий момент вре- мени 156 – X ⊆ {1, . . . , n} \ {i}, X = список активных процес- сов на текущий момент времени (т.е. таких процессов, которые начали очередной сеанс, но пока его не закон- чили) • начальное состояние планировщика имеет метку (1, ∅) • множество переходов состоит из – переходов вида s - α i ! s 0 где ∗ label(s) = (i, X) ∗ label(s 0 ) = (next(i), X ∪ {i}), где next(i) def = ( i + 1, если i < n, и 1, если i = n – и переходов вида s - β j ! s 0 где ∗ label(s) = (i, X), ∗ label(s 0 ) = (i, X \ {j}), причём j ∈ X Сформулированное описание свойств требуемого планировщика можно рассматривать как его определение: • в качестве множества состояний планировщика мы можем взять просто множество пар вида {(i, X) ∈ {1, . . . , n} × P({1, . . . , n}) | i 6∈ X} (т.е. каждое состояние совпадает со своей меткой) • и определить множество переходов так, как описано выше. Обозначим такой планировщик знакосочетанием Sch 0 Описание планировщика Sch 0 содержит существенный недо- статок: размер такого описания экспоненциально зависит от чис- ла процессов (6.7), которыми нужно управлять (число состояний 157 Sch 0 равно n·2 n−1 ), что не позволяет быстро модифицировать та- кой планировщик в том случае, когда множество процессов (6.7) изменяется (например, к нему добавляются новые процессы, или удаляются старые). Мы можем использовать Sch 0 только как эталон, с которым мы каким-либо способом будем сравнивать другие планировщи- ки. Для решения поставленной задачи мы определим другой пла- нировщик Sch. Мы будем определять его • не путём явного описания состояний и переходов, • а путём задания некоторого выражения, которое определя- ет его в терминах композиции процессов достаточно про- стого вида. Данное описание будет лишено сформулированного выше недо- статка. В описании планировщика Sch мы будем использовать новые вспомогательные имена γ 1 , . . . , γ n . Обозначим множество этих имён символом Γ. Процесс Sch определяется следующим образом: Sch def = (Start | C 1 | . . . | C n ) \ Γ (6.18) где • Start def = γ 1 !. 0 • для каждого i = 1, . . . , n процесс C i имеет вид ? - 6 γ i ? γ next(i) ! β i ! α i ! 158 Потоковый граф процесса Sch в случае n = 4 имеет следую- щий вид: ' & $ % ' & $ % ' & $ % ' & $ % ' & $ % u ? - 6 u e u u u e u u u e u u u e u u Start C 1 C 2 C 3 C 4 α 1 β 4 β 2 α 3 α 2 β 1 β 3 α 4 γ 2 γ 4 γ 3 γ 1 γ 1 Приведём неформальное пояснение функционирования процесса Sch. Назовём процессы C 1 , . . . , C n , участвующие в определении пла- нировщика Sch, циклерами. Циклер C i называется • выключенным, если он находится в своём начальном со- стоянии, и • включённым, если он находится не в начальном состоя- нии. Процесс Start включает первый циклер C 1 и после этого “уми- рает”. Каждый циклер C i отвечает за работу процесса P i . Циклер C i 159 • включает следующий циклер C next(i) после того, как он дал разрешение процессу P i начать очередной сеанс работы, и • выключается после того, как он дал разрешение процессу P i закончить очередной сеанс работы. Докажем, что процесс (6.18) удовлетворяет условию (6.17) (проверку условия (6.16) мы опустим). Согласно определению процесса (6.15), условие (6.17) имеет вид (Sch | (β 1 ?) ∗ | . . . | (β n ?) ∗ ) \ B ≈ (α 1 !. . . . α n !) ∗ (6.19) где B = {β 1 , . . . , β n }. Обозначим Sch 0 def = левая часть (6.19). Докажем, что Sch 0 + ≈ τ.α 1 !. . . . α n !. Sch 0 (6.20) Отсюда, по свойству единственности (с точностью до + ≈) решения уравнения X = τ.α 1 !. . . . α n !. X будет следовать соотношение Sch 0 + ≈ (τ α 1 ! . . . α n ! ) ∗ из которого, в свою очередь, следует (6.19). Мы будем преобразовывать левую часть соотношения (6.20) так, чтобы получилась правая часть этого соотношения. Для этого мы будем использовать свойства 8, 11 и 12 операций на процессах, сформулированные в параграфе 3.7. Напомним эти свойства: • P \ L = P , если L ∩ names(Act(P )) = ∅ • (P 1 | P 2 ) \ L = (P 1 \ L) | (P 2 \ L), если L ∩ names(Act(P 1 ) ∩ Act(P 2 )) = ∅ • (P \ L 1 ) \ L 2 = P \ (L 1 ∪ L 2 ) = (P \ L 2 ) \ L 1 160 Используя данные свойства, можно преобразовать левую часть соотношения (6.20) следующим образом. Sch 0 = = (Sch | (β 1 ?) ∗ | . . . | (β n ?) ∗ ) \ B = = ((Start | C 1 | . . . | C n ) \ Γ) | | (β 1 ?) ∗ | . . . | (β n ?) ∗ ! \ B = = (Start | C 0 1 | . . . | C 0 n ) \ Γ (6.21) где C 0 i = (C i | (β i ?) ∗ ) \ {β i } Заметим, что для каждого i = 1, . . . , n имеет место соотноше- ние C 0 i + ≈ γ i ?. α i !. γ next(i) !. C 0 i (6.22) Действительно, по теореме о разложении C 0 i = ((γ i ?. α i !. γ next(i) !. β i !. C i ) | (β i ?) ∗ ) \ {β i } ∼ ∼ γ i ?. α i !. γ next(i) !. τ.C 0 i + ≈ правая часть (6.22) Используя данное замечание и теорему о разложении, цепочку равенств (6.21) можно продолжить следующим образом: (Start | C 0 1 | C 0 2 | . . . | C 0 n ) \ Γ + ≈ + ≈(γ 1 !. 0 | {z } =Start | γ 1 ?. α 1 !. γ 2 !. C 0 1 | {z } + ≈ C 0 1 | C 0 2 | . . . | C 0 n ) \ Γ ∼ ∼ τ. (0 | α 1 !. γ 2 !. C 0 1 | C 0 2 | . . . | C 0 n ) \ Γ = = τ. (α 1 !. γ 2 !. C 0 1 | C 0 2 | . . . | C 0 n ) \ Γ ∼ ∼ τ. α 1 !. (γ 2 !. C 0 1 | C 0 2 | . . . | C 0 n ) \ Γ + ≈ + ≈ τ. α 1 !. (γ 2 !. C 0 1 | γ 2 ?. α 2 !. γ 3 !. C 0 2 | {z } + ≈ C 0 2 | . . . | C 0 n ) \ Γ ∼ ∼ τ. α 1 !. τ. (C 0 1 | α 2 !. γ 3 !. C 0 2 | . . . | C 0 n ) \ Γ ∼ . . . ∼ ∼ τ. α 1 !. τ. α 2 !. . . . τ. α n !. (C 0 1 | . . . | γ 1 !. C 0 n ) \ Γ + ≈ + ≈ τ. α 1 !. . . . α n !. (C 0 1 | . . . | γ 1 !. C 0 n ) \ Γ + ≈ + ≈ τ. α 1 !. . . . α n !. ( γ 1 ?. α 1 !. γ 2 !. C 0 1 | {z } + ≈ C 0 1 | . . . | γ 1 !. C 0 n ) \ Γ ∼ ∼ τ. α 1 !. . . . α n !. τ. (α 1 !. γ 2 !. C 0 1 | . . . | C 0 n ) \ Γ | {z } (6.23) 161 Выражение, подчёркнутое фигурной скобкой в последней стро- ке данной цепочки, совпадает с выражением в четвёртой строке этой цепочки, которое, в свою очередь, находится в отношении + ≈ с Sch 0 Мы получили, что последнее выражение в цепочке (6.23) • находится в отношении + ≈ с правой частью соотношения (6.20), и • с другой стороны, данное выражение находится в отноше- нии + ≈ с левой частью соотношения (6.20) Таким образом, соотношение (6.20) доказано. Читателю предоставляется в качестве упражнения доказать • истинность условия (6.16), и • соотношение Sch ≈ Sch 0 Читателю предлагается самостоятельно определить и дока- зать корректность планировщика, управляющего совокупностью P 1 , . . ., P n процессов с приоритетами, в которой каждому про- цессу P i сопоставлен некоторый приоритет, представляющий собой число p i ∈ [0, 1], причём P n i=1 p i = 1. Планировщик должен реализовать такой режим работы про- цессов P 1 , . . ., P n , при котором • для каждого i = 1, . . . , n доля количества сеансов, выпол- ненных процессом P i , относительно общего количества се- ансов, выполненных всеми процессами P 1 , . . . , P n , асимпто- тически стремилась бы к p i , при неограниченном увеличе- нии времени работы процессов P 1 , . . ., P n , причём • данный планировщик должен обеспечивать максимальную свободу функционирования процессов P 1 , . . . , P n 162 6.5 Семафор В этом примере, как и в примере из предыдущего параграфа, предполагается, что заданы n процессов P 1 , . . . , P n (6.24) причём для каждого i = 1, . . . , n процесс P i имеет вид P i = (α i ? a i1 . . . a ik i β i ?) ∗ где • α i ? и β i ? – служебные действия, представляющие собой сиг- налы о начале и о конце очередного сеанса работы процесса P i , и • a i1 , . . . , a ik i – собственные действия процесса P i Мы хотели бы создать такой процесс P , в котором все про- цессы P 1 , . . ., P n работали бы совместно, причём эта совместная работа должна подчиняться следующему режиму: • если в некоторый момент времени какой-либо из процессов P i начал очередной сеанс своей работы исполнением дей- ствия α i ?, • то этот сеанс должен быть непрерываемым, т.е. все по- следующие действия процесса P должны быть действиями процесса P i , до тех пор, пока P i не завершит этот сеанс. Данное требование можно выразить в терминах трасс: каждая трасса процесса P должна иметь вид α i ? a i1 . . . a ik i β i ? α j ? a j1 . . . a jk j β i ? . . . т.е. каждая трасса tr процесса P должна представлять собой конкатенацию трасс tr 1 · tr 2 · tr 3 каждая из которых представляет собой сеанс работы какого-либо процесса из (6.24). 163 Искомый процесс P мы определим следующим образом: P := ( P 1 [f 1 ] | . . . | P n [f n ] | Sem ) \ {π, ϕ} где • Sem – процесс, предназначенный для задания требуемого режима работы процессов P 1 , . . ., P n , данный процесс на- зывается семафором и имеет вид Sem = ( π! ϕ! ) ∗ • f i : α i 7→ π, β i 7→ ϕ Спецификация процесса P представляется следующим со- отношением: P + ≈ τ.a 11 . . . . a 1k 1 . P + . . . + + τ.a n1 . . . . a nk n . P (6.25) Доказательство того, что процесс P удовлетворяет этой специ- фикации, производится при помощи теоремы о разложении: P = ( P 1 [f 1 ] | . . . | P n [f n ] | Sem ) \ {π, ϕ} ∼ ∼ π?.a 11 . . . . .a 1k 1 .ϕ?.P 1 [f 1 ] | . . . | | π?.a n1 . . . . .a nk n ϕ?.P n [f n ] | | π!. ϕ!. Sem \ {π, ϕ} ∼ ∼ τ. a 11 . . . . .a 1k 1 .ϕ?.P 1 [f 1 ] | . . . | | π?.a n1 . . . . .a nk n ϕ?.P n [f n ] | | ϕ!. Sem \ {π, ϕ}+ + . . . + +τ. π?.a 11 . . . . .a 1k 1 .ϕ?.P 1 [f 1 ] | . . . | | a n1 . . . . .a nk n ϕ?.P n [f n ] | | ϕ!. Sem \ {π, ϕ} ∼ ∼ . . . ∼ ∼ τ.a 11 . . . . a 1k 1 .τ. P + . . . + τ.a n1 . . . . a nk n .τ. P + ≈ + ≈ τ.a 11 . . . . a 1k 1 . P + . . . + τ.a n1 . . . . a nk n . P В заключение обратим внимание на следующий момент. На- личие префикса “τ.” в каждом слагаемом в правой части соот- ношения (6.25) означает, что выбор альтернативы в начальный момент функционирования процесса P определяется 164 • не в окружающей среде процесса P , • а внутри процесса P . Если бы этого префикса не было, то это означало бы, что выбор альтернативы в начальный момент функционирования процесса P определяется окружающей средой процесса P . 165 Глава 7 Процессы с передачей сообщений 7.1 Действия с передачей сообщений Введённое и изученное в предыдущих главах понятие процесса допускает различные обобщения. Одно из таких обобщений заключается в добавлении к дей- ствиям из Act некоторых параметров, т.е. рассматриваются та- кие процессы, у которых выполняемые действия имеют вид (a, p) где a ∈ Act, и p – параметр, который может иметь, например следующий смысл: • сложность (или стоимость) выполнения действия a • приоритет действия a по отношению к другим действиям • момент времени, в который произошло действие a • длительность действия a • вероятность совершения действия a • или что-либо другое. 166 В настоящей главе мы рассматриваем один из вариантов та- кого обобщения, который связан с добавлением к действиям из Act параметров, представляющих собой сообщения, передавае- мые при выполнении этих действий. Напомним, что, согласно нашей неформальной интерпрета- ции понятия действия, • выполнение процессом действия вида α ! заключается в пе- редаче другому процессу объекта с именем α, и • выполнение процессом действия вида α ? заключается в по- лучении от другого процесса объекта с именем α. Обобщим данную интерпретацию следующим образом. Будем считать, что к объектам, которыми обмениваются процессы, мож- но добавлять сообщения, т.е. действия процессов могут иметь вид α ! v и α ? v (7.1) где α ∈ N ames, и v – сообщение, которое может представлять собой • число, • символьную строку, • банкноту, • материальный ресурс, • и т.п. Выполняя действие вида α ! v или α ? v, процесс передаёт или получает вместе с объектом α сообщение v. Напомним, что понятие передаваемого объекта, как и поня- тия приёма и передачи, могут иметь виртуальный характер (бо- лее подробно см. параграф 2.3). Для формального описания процессов, которые могут выпол- нять действия вида (7.1), мы обобщим понятие процесса. 167 7.2 Вспомогательные понятия 7.2.1 Типы, переменные, значения и константы Мы будем предполагать, что задано множество T ypes типов, причём каждому типу t ∈ T ypes сопоставлено множество D t зна- чений типа t. Типы могут обозначаться идентификаторами. Для наиболее часто используемых типов существуют общепринятые иденти- фикаторы, например, • тип целых чисел обозначается int • тип булевых значений (0 и 1) обозначается bool • тип “символы” обозначается char • тип “символьные строки” обозначается string Также мы будем предполагать, что заданы следующие мно- жества. • Множество V ar, элементы которого называются перемен- ными, причём каждой переменной x ∈ V ar сопоставлен тип t(x) ∈ T ypes. Каждая переменная x ∈ V ar может принимать значения в множестве D t(x) , т.е. в различные моменты времени пе- ременная x может быть связана с различными элементами множества D t(x) • Множество Con, элементы которого называются констан- тами. Каждой константе c ∈ Con сопоставлены – тип t(c) ∈ T ypes, и – значение [[c]] ∈ D t(c) , называемое интерпретацией кон- станты c. 168 7.2.2 Функциональные символы Мы будем предполагать, что задано множество функциональ- ных символов (ФС), причём каждому ФС f сопоставлены • функциональный тип t(f ) (называемый ниже просто типом), представляющий собой знакосочетание (t 1 , . . . , t n ) → t (7.2) где t 1 , . . . , t n , t ∈ T ypes, и • частичная функция [[f ]] : D t 1 × . . . × D t n → D t называемая интерпретацией ФС f . Например, ниже мы будем рассматривать следующие ФС: +, −, ·, head, tail, [ ] где • ФС + и − имеют тип (int, int) → int функции [[+]] и [[−]] представляют собой соответствующие арифметические операции • ФС · имеет тип (string, string) → string функция [[·]] сопоставляет каждой паре строк (u, v) строку, получаемую приписыванием v к u справа (т.е. конкатена- цию u и v). • ФС head имеет тип string → char функция [[head]] сопоставляет каждой непустой строке её первый символ (значение функции [[head]] на пустой строке не определено) 169 • ФС tail имеет тип string → string функция [[tail]] сопоставляет каждой непустой строке u стро- ку, получаемую из u удалением её первого символа (значение функции [[tail]] на пустой строке не определено) • ФС [ ] имеет тип char → string функция [[ [ ] ]] сопоставляет каждому символу строку, со- стоящую из одного этого символа • ФС length имеет тип string → int функция [[length]] сопоставляет каждой строке её длину (т.е. количество символов в этой строке). 7.2.3 Выражения Выражения строятся стандартным образом из переменных, кон- стант и ФС. Каждое выражение e имеет тип t(e) ∈ T ypes, опре- деляемый структурой этого выражения. Правила построения выражений имеют следующий вид. • Каждая переменная или константа является выражением того типа, который сопоставлен этой переменной или кон- станте. • Если – f – ФС, имеющий тип (7.2), и – e 1 , . . . , e n – выражения типов t 1 , . . . , t n соответственно то знакосочетание f (e 1 , . . . , e n ) является выражением типа t. 170 Если каждой переменной x, входящей в выражение e, сопо- ставлено значение ξ(x), то выражению e можно сопоставить зна- чение, обозначаемое знакосочетанием ξ(e), и определяемое стан- дартным образом: • если e = x (переменная), то ξ(e) def = ξ(x) (значение ξ(x) предполагается заданным) • если e = c (константа), то ξ(e) def = [[c]] • если e = f (e 1 , . . . , e n ), то значение ξ(e) выражения e опре- делено, если – все значения ξ(e 1 ), . . . , ξ(e n ) определены, и – значение функции [[f ]] определено на списке (ξ(e 1 ), . . . , ξ(e n )) в этом случае ξ(e) def = [[f ]](ξ(e 1 ), . . . , ξ(e n )) Ниже мы будем использовать следующие обозначения. • Знакосочетание Expr обозначает совокупность всех выра- жений. • Знакосочетание F m обозначает совокупность тех выраже- ний, которые имеют тип bool. Выражения из F m называются формулами. При построении формул могут использоваться обычные бу- левские связки (∧, ∨, → и т.д.), интерпретируемые стан- дартным образом. Символ > обозначает тождественно истинную формулу, а символ ⊥ – тождественно ложную формулу. Формулы вида ∧(b 1 , b 2 ), ∨(b 1 , b 2 ), и т.п. мы будем записы- вать в более привычном виде b 1 ∧ b 2 , b 1 ∨ b 2 , и т.д. 171 В некоторых случаях формулы вида b 1 ∧ . . . ∧ b n и b 1 ∨ . . . ∨ b n будут записываться в виде b 1 b n и b 1 b n соответственно. • Выражения вида +(e 1 , e 2 ), −(e 1 , e 2 ) и ·(e 1 , e 2 ) будут запи- сываться в более привычном виде e 1 + e 2 , e 1 − e 2 и e 1 · e 2 • Выражения вида head(e), tail(e), [ ](e), и length(e) будут записываться в виде ˆ e, e 0 , [e] и |e| соответственно. • Костанта, интерпретацией которой является пустая строка, будет обозначаться символом ε. 7.3 Понятие процесса с передачей сооб- щений В этом параграфе мы излагаем понятие процесса с передачей со- общений. Данное понятие получается из исходного понятия про- цесса, изложенного в параграфе 2.4, следующей модификацией. • К числу компонентов процесса добавляются – компонента X P , называемая множеством перемен- ных этого процесса, и – компонента I P , называемая начальным условием. • Метки переходов представляют собой не действия, а опе- раторы. Прежде чем излагать формальное определение понятия про- цесса с передачей сообщений, мы объясним смысл вышеперечис- ленных понятий. Для краткости, мы будем в этой главе называть процессы с передачей сообщений просто процессами. 172 7.3.1 Множество переменных процесса Мы будем предполагать, что с каждым процессом P связано мно- жество переменных X P ⊆ V ar В каждый момент времени i работы процесса P (i = 0, 1, 2, . . .) каждой переменной x ∈ X P сопоставлено значение ξ i (x) ∈ D t(x) Значения переменных могут изменяться во время работы процес- са. Означиванием переменных из X P называется произволь- ный набор ξ значений, сопоставленных этим переменным, т.е. каждое означивание ξ имеет вид ξ = {ξ(x) ∈ D t(x) | x ∈ X P } Таким образом, в каждый момент времени i работы процесса P определено некоторое означивание ξ i переменных из X P Для каждого процесса P знакосочетание Eval(X P ) обознача- ет совокупность всевозможных означиваний переменных из X P Ниже мы будем предполагать, что для каждого процесса P все выражения, относящиеся к процессу P , содержат переменные только из множества X P 7.3.2 Начальное условие Другой новой компонентой процесса P является формула I P ∈ F m, называемая начальным условием. Данная формула вы- ражает условие на означивание ξ 0 переменных процесса P в на- чальный момент его работы: ξ 0 должно удовлетворять условию ξ 0 (I P ) = 1 7.3.3 Операторы Главное отличие нового определения понятия процесса от старо- го заключается в том, что • в старом определении метка каждого перехода является действием, которое совершает процесс при выполнении этого перехода, а 173 • в новом определении метка каждого перехода является опе- ратором, который представляет собой схему действия, приобретающую вид конкретного действия лишь при кон- кретном выполнении этого оператора. В определении понятия оператора мы будем использовать то же самое множество N ames, которое было введено в параграфе 2.3. Обозначим символом O множество, элементы которого назы- ваются операторами, и подразделяются на следующие четыре класса. 1. Операторы ввода, которые представляют собой знакосо- четания вида α ? x (7.3) где α ∈ N ames и x ∈ V ar. Действие, соответствующее оператору (7.3), выполняется путём ввода в процесс объекта, который имеет • имя α, и • дополнительный параметр, представляющий собой со- общение. Введённое сообщение v записывается в переменную x, т.е. после исполнения данного действия значение переменной x становится равным v. 2. Операторы вывода, которые представляют собой знако- сочетания вида α ! e (7.4) где α ∈ N ames и e ∈ Expr. Действие, соответствующее оператору (7.4), исполняется путём вывода из процесса объекта, который имеет • имя α, и • дополнительный параметр, представляющий собой со- общение вида v, которое равно значению выражения e на текущих значениях переменных процесса. 174 3. Операторы присваивания (первый вид внутренних опера- торов), которые представляют собой знакосочетания вида x := e (7.5) где • x ∈ V ar, и • e ∈ Expr, причём t(e) = t(x) Действие, соответствующее оператору (7.5), исполняется путём обновления значения переменной x: после исполне- ния этого оператора её значение становится равным значе- нию выражения e на текущих значениях переменных про- цесса P |