Теория процессов
 Скачать 1.62 Mb.
|
|
(k > 0) ? Out ! ˆ q q := q 0 k := k − 1 его начальное условие – (k = 0) ∧ (q = ε), и • Buf – процесс, имеющий вид b a - Out ! x In ? x начальное условие этого процесса = >. 219 Определим функцию µ : {A} × {a, b} → F m следующим об- разом: µ(A, a) def = (k = 0) ∧ (q = ε) µ(A, b) def = (k = 1) ∧ (q = [x]) Проверим свойства 1, 2, и 3 для функции µ. 1. Свойство 1 в данном случае представляет собой неравен- ство ((k = 0) ∧ (q = ε)) ∧ > ≤ ((k = 0) ∧ (q = ε)) которое, очевидно, верно. 2. Проверим свойство 2. • Для пары (A, a) нам надо рассмотреть лишь левый пе- реход в процессе Buffer 1 (так как для правого перехода не выполнено условие (7.26)). В качестве (7.27) мы возьмем совокупность, состоя- щую из единственного перехода из a в b. Диаграмма (7.29) в данном случае имеет вид A a (k = 0) ∧ (q = ε) ? k < 1 In ? f q := q · [f ] k := k + 1 ? In ? x A b (k = 1) ∧ (q = [x]) (7.32) Пользуясь тем, что ∀ ϕ, ψ, θ ∈ F m (ϕ ≤ ψ → θ ⇔ ϕ ∧ ψ ≤ θ) (7.33) 220 запишем неравенство, соответствующее этой диаграм- ме, в виде k = 0 q = ε k < 1 ≤ ( k + 1 = 1 q · [z] = [z] ) (7.34) Очевидно, что данное неравенство верно. • Для пары (A, b) нам надо рассмотреть лишь правый переход в процессе Buffer 1 (так как для левого пере- хода не выполнено условие (7.26)). В качестве (7.27) мы возьмем совокупность, состоя- щую из единственного перехода из b в a. Диаграмма (7.29) в данном случае имеет вид A b (k = 1) ∧ (q = [x]) ? k > 0 Out ! ˆ q q := q 0 k := k − 1 ? Out ! x A a (k = 0) ∧ (q = ε) (7.35) Пользуясь (7.33), запишем неравенство, соответствую- щее этой диаграмме, в виде k = 1 q = [x] k > 0 ≤ ˆ q = x k − 1 = 0 q 0 = ε (7.36) Очевидно, что это неравенство верно. 3. Проверим свойство 3. 221 • Для пары (A, a) и для единственного перехода из a в b в качестве (7.30) мы возьмем совокупность, состоящую из левого перехода из A в A. Диаграмма (7.31) в данном случае имеет вид (7.32). Как уже было установлено, данная диаграмма верна. • Для пары (A, b) и для единственного перехода из b в a в качестве (7.30) мы возьмем совокупность, состоящую из правого перехода из A в A. Диаграмма (7.31) в данном случае имеет вид (7.35). Как уже было установлено, данная диаграмма верна. 7.8.14 Дополнительные замечания Для повышения удобства применения теоремы 34 можно исполь- зовать следующие понятия и утверждения. Инварианты процессов Пусть P – процесс с СО. Формула Inv с переменными из X P называется инвариан- том процесса P , если она обладает следующими свойствами. • I P ≤ Inv • для каждого перехода s - Op s 0 процесса P – если Op – внутренний, то Inv ≤ Op(Inv) – если Op – СО ввода, и имеет вид Op 1 · (α ? x) · Op 2 , то Inv ≤ (Op 1 · (x := z) · Op 2 )(Inv) где z – переменная, не входящая в X P – если Op – СО вывода, и имеет вид Op 1 · (α ! e) · Op 2 , то Inv ≤ (Op 1 · Op 2 )(Inv) С использованием понятия инварианта процесса теорему 34 можно модифицировать следующим образом. Теорема 35. Пусть 222 • P 1 и P 2 – два процесса с СО: P i = (X P i , I P i , S P i , s 0 P i , R P i ) (i = 1, 2) не имеющие общих состояний и общих переменных, и • формулы Inv 1 и Inv 2 являются инвариантами процессов P 1 и P 2 соответственно. P 1 и P 2 находятся в отношении ≈, если существует функция µ вида µ : S P 1 × S P 2 → F m обладающая следующими свойствами. 1. I P 1 ∧ I P 2 ≤ µ(s 0 P 1 , s 0 P 2 ). 2. Для • каждой пары (A 1 , A 2 ) ∈ S P 1 × S P 2 , и • каждого перехода A 1 - Op A 0 1 процесса P 1 , такого, что cond (Op) µ(A 1 , A 2 ) Inv 1 Inv 2 6= ⊥ (7.37) существует совокупность СП процесса P 2 с началом A 2 { A 2 - CT i A i 2 | i ∈ =} (7.38) удовлетворяющая следующим условиям: (a) имеет место неравенство cond (Op) µ(A 1 , A 2 ) Inv 1 Inv 2 ≤ _ i∈= cond (CT i ) (7.39) 223 (b) для каждого i ∈ = верна диаграмма A 1 A 2 µ(A 1 , A 2 ) Inv 1 Inv 2 ? Op ? CT i A 0 1 A i 2 µ(A 0 1 , A i 2 ) (7.40) 3. Свойство, симметричное предыдущему: для • каждой пары (A 1 , A 2 ) ∈ S P 1 × S P 2 , и • каждого перехода A 2 - Op A 0 2 процесса P 2 , такого, что верно (7.37) существует совокупность СП процесса P 1 с началом A 1 { A 1 - CT i A i 1 | i ∈ =} (7.41) удовлетворяющая следующим условиям: (a) имеет место неравенство (7.39) (b) для каждого i ∈ = верна диаграмма 224 A 1 A 2 µ(A 1 , A 2 ) Inv 1 Inv 2 ? CT i ? Op A i 1 A 0 2 µ(A i 1 , A 0 2 ) (7.42) Композиция диаграмм Теорема 36. Пусть • ϕ, ψ, θ – формулы • Op 1 , Op 2 – внутренние СО, такие, что верна диаграмма A B ϕ ? Op 1 ? Op 2 C D ψ • Op 0 1 , Op 0 2 – СО, такие, что верна диаграмма 225 C D ψ ? Op 0 1 ? Op 0 2 E F θ • {Op 1 , Op 0 1 } и {Op 2 , Op 0 2 } не имеют общих переменных. Тогда верна диаграмма A B ϕ ? Op 1 · Op 0 1 ? Op 2 · Op 0 2 E F θ 7.8.15 Другой пример доказательства наблю- даемой эквивалентности процессов с СО В качестве примера использования теорем из параграфа 7.8.14 докажем наблюдаемую эквивалентность • процесса (Buffer n 1 [P ass/Out] | Buffer n 2 [P ass/In]) \ {P ass} (7.43) 226 где P ass 6∈ {In, Out}, и • процесса Buffer n 1 +n 2 Процесс (7.43) представляет собой последовательную компо- зицию даух буферов размеров n 1 и n 2 . Его потоковый граф имеет вид ' & $ % ' & $ % e u u e - Buffer n 1 Buffer n 2 In Out P ass Согласно определению операций на процессах с СО (см. па- раграф 7.8.5), графовое представление процесса (7.43) выглядит следующим образом: A - (k 1 < n 1 ) ? In ? f 1 q 1 := q 1 · [f 1 ] k 1 := k 1 + 1 (k 2 > 0) ? Out ! ˆ q 2 q 2 := q 0 2 k 2 := k 2 − 1 6 (k 1 > 0) ∧ (k 2 < n 2 ) ? f 2 := ˆ q 1 q 1 := q 0 1 k 1 := k 1 − 1 q 2 := q 2 · [f 2 ] k 2 := k 2 + 1 (7.44) Начальным условием процесса (7.44) является формула ( (n 1 > 0) ∧ (k 1 = 0) ∧ (q 1 = ε) (n 2 > 0) ∧ (k 2 = 0) ∧ (q 2 = ε) ) Графовое представление процесса Buffer n 1 +n 2 имеет вид 227 a - (k < n 1 + n 2 ) ? In ? f q := q · [f ] k := k + 1 (k > 0) ? Out ! ˆ q q := q 0 k := k − 1 Начальным условием процесса Buffer n 1 +n 2 является формула (n 1 + n 2 > 0) ∧ (k = 0) ∧ (q = ε) Нетрудно проверить, что формула Inv def = 0 ≤ k 1 ≤ n 1 |q 1 | = k 1 0 ≤ k 2 ≤ n 2 |q 2 | = k 2 n 1 > 0 n 2 > 0 является инвариантом процесса (7.44). Этот факт следует, в част- ности, из истинности для каждой строки u и каждого символа a соотношений ( |u| > 0 ⇒ |u 0 | = |u| − 1 |u · [a]| = |[a] · u| = |u| + 1 В качестве инварианта второго процесса мы возьмём формулу >. Определим функцию µ : {A} × {a} → F m следующим обра- зом: µ(A, a) def = ( q = q 2 · q 1 k = k 2 + k 1 ) Проверим свойства 1, 2, и 3 для функции µ. 1. Свойство 1 в данном случае представляет собой неравен- ство (n 1 > 0) ∧ (k 1 = 0) ∧ (q 1 = ε) (n 2 > 0) ∧ (k 2 = 0) ∧ (q 2 = ε) (n 1 + n 2 > 0) ∧ (k = 0) ∧ (q = ε) ≤ ( q = q 2 · q 1 k = k 2 + k 1 ) которое, очевидно, верно. 228 2. Проверим свойство 2. • Для левого перехода процесса (7.44) неравенство (7.37) верно. В качестве (7.38) мы возьмем совокупность, един- ственным элементом которой является левый переход процесса Buffer n 1 +n 2 Неравенство (7.39) в данном случае имеет вид k 1 < n 1 q = q 2 · q 1 k = k 2 + k 1 Inv ≤ (k < n 1 + n 2 ) что, очевидно, верно. Пользуясь (7.33), запишем неравенство, соответствую- щее диаграмме (7.40) для данного случая в виде q = q 2 · q 1 k = k 2 + k 1 Inv k 1 < n 1 k < n 1 + n 2 ≤ ( q · [z] = q 2 · q 1 · [z] k + 1 = k 2 + k 1 + 1 ) (7.45) Нетрудно установить, что последнее неравенство вер- но. • Для среднего (внутреннего) перехода процесса (7.44) неравенство (7.37) верно. В качестве (7.38) мы возь- мем совокупность, единственным элементом которой является пустой СП процесса Buffer n 1 +n 2 Неравенство (7.39) в данном случае верно по триви- альной причине: правая часть в нём имеет вид >. Пользуясь соотношением (7.33), запишем неравенство, соответствующее диаграмме (7.40) для данного слу- чая, в виде q = q 2 · q 1 k = k 2 + k 1 Inv k 1 > 0 k 2 < n 2 ≤ ( q = (q 2 · [ˆ q 1 ]) · q 0 1 k = k 2 + 1 + k 1 − 1 ) (7.46) 229 Данное неравенство следует из – ассоциативности операции конкатенации, и – истинности для каждой строки u соотношения |u| > 0 ⇒ u = [ˆ u] · u 0 • Для правого перехода процесса (7.44) неравенство (7.37) верно. В качестве (7.38) мы возьмем совокупность, един- ственным элементом которой является правый пере- ход процесса Buffer n 1 +n 2 Неравенство (7.39) в данном случае имеет вид k 2 > 0 q = q 2 · q 1 k = k 2 + k 1 Inv ≤ (k > 0) что, очевидно, верно. Пользуясь соотношением (7.33), запишем неравенство, соответствующее диаграмме (7.40) для данного слу- чая, в виде q = q 2 · q 1 k = k 2 + k 1 Inv k 2 > 0 k > 0 ≤ ˆ q 2 = ˆ q q 0 = q 0 2 · q 1 k − 1 = k 2 − 1 + k 1 (7.47) Данное неравенство следует из истинности для каж- дой пары строк u, v соотношения |u| > 0 ⇒ ( (u · v)ˆ = ˆ u (u · v) 0 = u 0 · v ) 3. Проверим свойство 3. • Для левого перехода процесса Buffer n 1 +n 2 неравенство (7.37) верно. В качестве (7.41) мы возьмем совокуп- ность, состоящую из двух СП: 230 – левого перехода процесса (7.44), и – последовательности из пары переходов, ∗ первым элементов которой является средний (внутренний) переход процесса (7.44), ∗ а вторым – левый переход процесса (7.44) Неравенство (7.39) в данном случае имеет вид k < n 1 + n 2 q = q 2 · q 1 k = k 2 + k 1 Inv ≤ (k 1 < n 1 ) ∨ k 1 > 0 k 2 < n 2 k 1 − 1 < n 1 Это неравенство верно (при его обосновании использу- ется содержащийся в Inv конъюнктивный член n 1 > 0). Истинность неравенств, соответствующих диаграммам (7.42) для обоих элементов совокупности (7.41), следу- ет из (7.45), (7.46) и теоремы 36. • Для правого перехода процесса Buffer n 1 +n 2 неравен- ство (7.37) верно. В качестве (7.41) мы возьмем сово- купность, состоящую из двух СП: – правого перехода процесса (7.44), и – последовательности из пары переходов, ∗ первым элементов которой является средний (внутренний) переход процесса (7.44), ∗ а вторым – правый переход процесса (7.44) Неравенство (7.39) в данном случае имеет вид k > 0 q = q 2 · q 1 k = k 2 + k 1 Inv ≤ (k 2 > 0) ∨ k 1 > 0 k 2 < n 2 k 2 + 1 > 0 Это неравенство верно (при его обосновании использу- ется содержащийся в Inv конъюнктивный член n 2 > 0). 231 Истинность неравенств, соответствующих диаграммам (7.42) для обоих элементов совокупности (7.41), следу- ет из (7.46), (7.47) и теоремы 36. 7.9 Рекурсивные определения процессов Для процессов с передачей сообщений можно ввести понятие ре- курсивного определения, которое аналогично понятию РО, изложенному в главе 5. РО для процессов с передачей сообщений очень похожи на функциональные программы. Понятие РО определяется на основе понятия процессного выражения (ПВ), которое почти совпадает с соответствующим понятием из параграфа 5.1, поэтому мы лишь укажем отличия в определениях этих понятий. • Во всех ПВ вместо действий используются операторы. • Каждое процессное имя A имеет тип t(A), который пред- ставляет собой последовательность обычных типов из T ypes: t(A) = (t 1 , . . . , t n ) (n ≥ 0) • Каждое процессное имя A входит в каждое ПВ только вме- сте со списком выражений соответствующих типов, т.е. каж- дое вхождение процессного имени A в произвольное ПВ со- держится в подвыражении вида A(e 1 , . . . , e n ), где (t(e 1 ), . . . , t(e n )) = t(A) Каждому ПВ P соответствует совокупность f v(P ) свобод- ных переменных этого ПВ, которая состоит из всех перемен- ных, имеющих свободные вхождения в P . Понятие свободного и связанного вхождения переменной в ПВ определяется почти так же, как определяется аналогичное понятие в логике предикатов, только в случае ПВ роль кванто- ров играют операторы ввода и присваивания: каждое свободное вхождение переменной x в ПВ P становится связанным в ПВ (α?x).P и в ПВ (x := e).P . 232 Рекурсивное определение (РО) процессов представляет собой список формальных равенств вида A 1 (x 11 , . . . , x 1k 1 ) = P 1 A n (x n1 , . . . , x nk n ) = P n (7.48) где • A 1 , . . . , A n – процессные имена, • для каждого i = 1, . . . , n список (x i1 , . . . , x ik i ) в левой ча- сти i–го равенства представляет собой список различных переменных • P 1 , . . . , P n – ПВ, которые удовлетворяют – условиям, изложенным в определении РО в параграфе 5.2, – а также следующему условию: для каждого i = 1, . . . , n совокупность {x i1 , . . . , x ik i } совпадает с совокупностью f v(P i ) свободных переменных ПВ P i РО (7.48) можно интерпретировать как функциональную про- грамму, состоящую из рекурсивных определений функций A 1 (x 11 , . . . , x 1k 1 ), . . . , A n (x n1 , . . . , x nk n ) Для каждого i = 1, . . . , n переменные x i1 , . . ., x ik i можно рассмат- ривать как формальные параметры функции A i (x i1 , . . . , x ik i ). Читателю предлагается самостоятельно определить соответ- ствие, которое сопоставляет каждому ПВ вида A(x 1 , . . . , x n ), где • A – процессное имя, и • x 1 , . . . , x n – список различных переменных соответствую- щих типов процесс [[A(x 1 , . . . , x n )]]. Примеры процессов, задаваемых в виде РО, будут изложены в главе 9. Проблемы, связанные с РО в случае процессов с передачей сообщений, имеют тот же вид, что и для обычных РО: 233 • распознавание существования конечных процессов, эквива- лентных процессам вида [[A(x 1 , . . . , x n )]] • построение алгоритмов нахождения минимальных процес- сов, эквивалентных процессам вида [[A(x 1 , . . . , x n )]] в том случае, когда эти процессы конечны • распознавание эквивалентности процессов вида [[A(x 1 , . . . , x n )]] • распознавание эквивалентности РО • нахождение необходимых и достаточных условий единствен- ности списка процессов, определяемого РО. 234 Глава 8 Примеры процессов с передачей сообщений 8.1 Разделение множеств 8.1.1 Задача разделения множеств Пусть задана пара U, V конечных непересекающихся множеств, причём каждому элементу x ∈ U ∪ V сопоставлено некоторое число w(x), называемое весом этого элемента. Требуется преобразовать эту пару в такую пару множеств U 0 , V 0 , чтобы • |U | = |U 0 |, |V | = |V 0 | (для каждого конечного множества M знакосочетание |M | обозначает количество элементов в M ) • для каждого u ∈ U 0 и каждого v ∈ V 0 выполнялось нера- венство w(u) ≤ w(v) 8.1.2 Распределённый алгоритм решения зада- чи разделения множеств Задачу разделения множеств можно решить путём выполнения нескольких сеансов обмена элементами между этими множества- ми. Каждый сеанс состоит из следующих действий: 235 • нахождение элемента mx с максимальным весом в левом множестве • нахождение элемента mn с минимальным весом в правом множестве • перенесение – mx из левого множества в правое, и – mn из правого множества в левое. Для реализации этой идеи предлагается использовать распре- делённый алгоритм, определяемый как процесс вида (Small | Large) \ {α, β} (8.1) где • процесс Small выполняет операции, связанные с левым мно- жеством, и • процесс Large выполняет операции, связанные с правым множеством. Потоковый граф, соответствующий этому алгоритму, имеет вид ' & $ % ' & $ % e u u e - α β Small Large Ниже мы будем использовать следующие обозначения: • для каждого подмножества W ⊆ U ∪ V знакосочетания max(W ) и min(W ) обозначают элемент множества W с мак- симальным и минимальным весом соответственно, • для 236 – любых подмножеств W 1 , W 2 ⊆ U ∪ V , и – любого u ∈ U ∪ V выражения W 1 ≤ u, u ≤ W 1 , W 1 ≤ W 2 являются сокращённой записью выражений ∀x ∈ W 1 w(x) ≤ w(u) ∀x ∈ W 1 w(u) ≤ w(x) ∀x ∈ W 1 , ∀y ∈ W 2 w(x) ≤ w(y) соответственно Аналогичный смысл имеют выражения max(W ), min(W ), W ≤ u, u ≤ W, W 1 ≤ W 2 в которых символы W , W i и u обозначают переменные, значени- ями которых являются • помножества множества U ∪ V , и • элементы множества U ∪ V соответственно. 8.1.3 Процессы Small и Large Процессы Small и Large могут быть определены в виде блок-схем, которые затем можно преобразовать в процессы с СО и редуци- ровать. Мы не будем давать описания этих блок-схем и излагать их преобразование в процессы с СО и этапы их редукции, при- ведём лишь соответствующие редуцированные процессы с СО. Процесс Small имеет следующий вид: Init = (S = U ) 237 |