Теория процессов
 Скачать 1.62 Mb.
|
|
timeout ? C ? - - Операторы, входящие в эту блок-схему, имеют следующий смысл. • In ? x – получение отправителем очередного пакета от своего СУ, и запись этого пакета в переменную x • C ! ϕ(x) – отправление в канал связи кадра ϕ(x) • start ! – включение таймера • timeout ? – получение от таймера сигнала timeout • C ? – получение из канала связи сигнала подтвержде- ния Процесс, представляемый этой блок-схемой, обозначается знакосочетанием Sender и имеет следующий вид: 260 A B C D ? - - In ? x start ! 6 timeout ? C ! ϕ(x) H H H H H H H H H H H H H H H H H H Y C ? Процесс отправителя является параллельной компози- цией (с ограничением) • процесса Sender, и • процесса Timer, представляющего поведение таймера, и имеющего вид - start ? t := 1 (t = 1)? timeout ! t := 0 (8.21) Начальное условие процесса Timer: t = 0. В этой модели мы не детализируем величину проме- жутка времени между – запуском таймера (действие start?), и – посылкой им сигнала timeout. 2. Канал связи (называемый ниже просто каналом) в каж- дый момент времени может содержать не более одного кад- ра или сигнала. Он может выполнять следующие действия: • получение кадра от отправителя, и – пересылка этого кадра получателю, или – пересылка получателю искажённого кадра, или 261 – потеря кадра • получение сигнала подтверждения от получателя, и – пересылка этого сигнала отправителю, или – потеря сигнала. Поведение канала представляется следующим процессом: α β γ - S ? y R ! y - R ? S ! ? > ? 6 R ! ∗ ? > ? (8.22) В этом процессе мы используем следующую абстракцию: символ ‘∗’ означает “искажённый кадр”. Мы не уточняем, как именно искажаются кадры в канале. Каждый кадр, по- ступивший в канал • либо передаётся из канала в неизменном виде получа- телю, • либо пребразуется в абстрактное значение ‘∗’, и это значение передаётся из канала получателю • либо пропадает, что выражается переходом процесса (8.22) с меткой > ? 3. Получатель периодически выполняет следующие действия: • получение из канала очередного кадра • проверка наличия искажений в кадре • если кадр не искажён, то – извлечение из кадра пакета, 262 – передача этого пакета процессу, называемому се- тевой уровень (СУ) получателя (этот процесс не входит в протокол) – посылка отправителю через канал сигнала под- тверждения • если кадр искажён, то получатель его игнорирует (пред- полагая, что отправитель, не дождавшись подтвержде- ния, пошлёт это кадр ещё раз) Блок-схема, представляющая описанное выше поведение, выглядит следующим образом: start ? ? C ? f f = ∗ Out ! info(f ) C ! - - − + s a s b s c Операторы, входящие в эту блок-схему, имеют следующий смысл. • C ? f – получение из канала очередного кадра, и запись его в переменную f • (f = ∗) – проверка наличия искажения в кадре f • Out ! info(f ) – отправление пакета info(f ), извлечённо- го из кадра f , своему СУ • C ! – посылка сигнала подтверждения Процесс, представляемый этой блок-схемой, обозначается знакосочетанием Receiver и имеет следующий вид: 263 a b c ? 6 C ? f f = ∗ - H H H H H H H H H H H H H H H H H H Y C ! (f 6= ∗) ? Out ! info(f ) Процесс Protocol, соответствующий всему протоколу, опреде- ляется как параллельная композиция (с ограничением) вышепе- речисленных процессов: Protocol def = Sender [S/C] | T imer | Channel | Receiver [R/C] \ {S, R, start, timeout} (8.23) Потоковый граф этого процесса имеет следующий вид: e u u e u e e u e u e u u e ? 6 start timeout S S R R ' & $ % Channel ' & $ % Sender T imer ' & $ % Receiver - - In Out (8.24) 264 Для того, чтобы можно было анализировать корректность этого протокола, необходимо точно определить спецификацию, которой он должен соответствовать. Если мы хотим специфицировать только свойства внешних действий, выполняемых этим протоколом (т.е. действий, име- ющих вид In ? v и Out ! v), то спецификация может выглядеть следующим образом: поведение данного протокола совпадает с поведением буфера размера 1, т.е. процесс Protocol наблюдаемо эквивалентен процессу Buf , который имеет вид 1 2 - In ? x Out ! x (8.25) При построении процесса с СО, соответствующего выраже- нию (8.23), и его редукции, получается диаграмма 6 ? * H H H H H H H H Y In ? x > ? > ? y := ϕ(x) f := y Out ! info(f ) которая наблюдаемо эквивалентна диаграмме 6 ? * H H H H H H H H Y In ? x > ? > ? Out ! info(ϕ(x)) (8.26) 265 Если мы предположим, что функция info извлечения паке- тов из кадров является обратной к функции ϕ формирования кадров, т.е. для каждого пакета x имеет место соотношение info(ϕ(x)) = x то диаграмму (8.26) можно перерисовать следующим образом: 6 ? * H H H H H H H H Y In ? x > ? > ? Out ! x (8.27) Процесс (8.27) можно редуцировать, в результате чего полу- чается процесс - In ? x Out ! x Out ! x (8.28) При сопоставлении процессов (8.28) и (8.25) можно заклю- чить, что данные процессы не могут быть эквивалентными ни в каком приемлемом смысле. Например, • процесс (8.25) после получения пакета x может только – передать этот пакет СУ получателя, и – перейти в состояние ожидания следующего пакета • в то время как процесс (8.28) может после получения пакета x передать этот пакет СУ получателя несколько раз. Такая повторная передача может происходить, например, при следующем варианте работы протокола. 266 • Первый кадр, посланный отправителем, доходит до полу- чателя успешно. • Получатель – пересылает пакет, извлечённый из этого кадра, своему СУ, и – посылает отправителю через канал подтверждение. • Это подтверждение пропадает в канале. • Отправитель, не дождавшись подтверждения, посылает этот кадр ещё раз, и этот кадр снова доходит успешно. • Получатель воспринимает этот кадр как новый. Он – пересылает пакет, извлечённый из этого кадра, своему СУ, и – посылает отправителю через канал подтверждение, ко- торое опять пропадает канале. • и т.д. Эта ситуация может возникнуть потому, что в данном прото- коле отсутствует механизм, с помощью которого получатель мог бы отличить новый кадр от переданного повторно. В следующем параграфе мы приводим пример протокола, в котором этот механизм присутствует. Для такого протокола уже можно формально доказать его соответствие спецификации (8.25). 8.4.5 Протокол с чередующимися битами Протокол с чередующимися битами (называемый в англо- язычной литературе словосочетанием Alternating Bit Protocol, или, сокращённо, ABP) предназначен для решения той же зада- чи, что и предыдущий протокол: доставка кадров от отправите- ля получателю через ненадёжный канал связи (который может искажать и терять передаваемые кадры). 267 Механизм, с помощью которого получатель может отличить новый кадр от переданного повторно, реализован в данном про- токоле следующим образом: среди переменных отправителя и по- лучателя присутствуют булевы переменные s и r соответственно, значения которых имеют следующий смысл: • значение переменной s равно чётности номера очередного кадра, которого пытается послать отправитель, и • значение переменной r равно чётности номера очередного кадра, которого ожидает получатель. В начальный момент значения s и r равны 0 (первый кадр имеет номер 0). Как и в предыдущем протоколе, в этом протоколе использу- ется абстрактное значение ‘∗’, обозначающее искажённый кадр. Работа протокола происходит следующим образом. 1. Отправитель, получив очередной пакет от своего СУ, • записывает его в переменную x, • формирует кадр, который представляет собой значе- ние некоторой кодирующей функции ϕ на паре (x, s), • посылает этот кадр в канал, • запускает таймер • после чего он ожидает подтверждение посланного кад- ра. Если у отправителя истекает время ожидания, и он не по- лучает подтверждения от получателя, то он повторно по- сылает уже посланный кадр. Если же он получает подтверждение, которое представляет собой неискажённый кадр, содержащий бит, то он анализи- рует значение этого бита: если оно совпадает с текущим значением s, то отправитель • инвертирует значение переменной s (используя для это- го функцию inv(x) = 1 − x), и 268 • начинает новый цикл своей работы. В противном случае он опять посылает уже посланный кадр. Блок-схема, представляющая такое поведение, выглядит сле- дующим образом: ' & $ % start s = 0 ? s A s B s C s D s E In ? x ? C ! ϕ(x, s) ? start ! ? timeout ? C ? z - inv(s) bit(z) = s z = ∗ 6 - 6 6 6 − + + − Процесс, представляемый этой блок-схемой, обозначается знакосочетанием Sender и имеет следующий вид: Init = (s = 0) 269 A B C D E ? - - 6 ( z 6= ∗ bit(z) = s ) ? inv(s) " z = ∗ bit(z) 6= s # ? In ? x C ? z C ! ϕ(x, s) start ! 6 timeout ? Процесс отправителя является параллельной компози- цией (с ограничением) процесса Sender, и процесса Timer. 2. Канал в каждый момент времени может содержать не бо- лее одного кадра. Он может выполнять следующие дей- ствия: • получение кадра от отправителя, и – пересылка этого кадра получателю, или – пересылка получателю искажённого кадра, или – потеря кадра • получение кадра с подтверждением от получателя, и – пересылка этого кадра отправителю, или – пересылка отправителю искажённого кадра, или – потеря кадра. Поведение канала представляется следующим процессом: 270 α β γ - S ? y R ! y - R ? u S ! u ? > ? 6 R ! ∗ ? > ? 6 S ! ∗ (8.29) 3. Получатель при получении очередного кадра из канала • проверяет, не искажён ли этот кадр, • и если не искажён, то извлекает из него пакет и свя- занный с ним бит при помощи функций info и bit, об- ладающих следующими свойствами: info(ϕ(x, b)) = x, bit (ϕ(x, b)) = b Получатель проверяет, совпадает ли значение бита, извле- чённого из кадра, с ожидаемым значением, которое содер- жится в переменной r. Если проверка дала положительный результат, то получа- тель • передаёт пакет, извлечённый из этого кадра, своему СУ • инвертирует значение переменной r, и • посылает отправителю через канал подтверждение. Если проверка дала отрицательный результат, то получа- тель посылает кадр подтверждения с неверным битом (что заставит отправителя послать свой кадр ещё раз). Если же кадр искажён, то получатель его игнорирует (пред- полагая, что отправитель, не дождавшись подтверждения, пошлёт это кадр ещё раз) 271 Блок-схема, представляющая описанное выше поведение, выглядит следующим образом: ' & $ % start r = 0 ? ? C ? f f = ∗ bit(f ) = r Out ! info(f ) inv(r) C ! ϕ(1 − r) 6 6 - - - − + + − s a s b s c Процесс, представляемый этой блок-схемой, обозначается знакосочетанием Receiver и имеет следующий вид: Init = (r = 0) a b c ? 6 C ? f f = ∗ - - H H H H H H H H H H H H H H H H H H Y C ! ϕ(1 − r) ( f 6= ∗ bit(f ) 6= r ) ? ( f 6= ∗ bit(f ) = r ) ? Out ! info(f ) inv(r) Процесс Protocol, соответствующий всему протоколу, опреде- ляется так же, как и в предыдущем пункте, выражением (8.23). Потоковый граф данного процесса имеет вид (8.24). 272 Спецификация данного протокола тоже имеет такой же вид, т.е. представляет собой процесс (8.25). При построении процесса с СО, соответствующего данному протоколу, и его последующей редукции, получается следующая диаграмма: i j - (s 6= r) ? inv(s) In ? x 6 ? (s 6= r) ? (s = r) ? Out ! x inv(s) inv(r) (s = r) ? Out ! x inv(r) (8.30) Доказать наблюдаемую эквивалентность процессов (8.25) и (8.30) можно, например, при помощи теоремы 34, определив функ- цию µ вида µ : {1, 2} × {i, j} → F m следующим образом: µ(1, i) def = (s = r) µ(2, i) def = ⊥ µ(1, j) def = (s 6= r) µ(2, j) def = (s = r) 8.4.6 Двунаправленная передача Рассмотренные выше протоколы относятся к классу симплекс- ных протоколов: они реализуют однонаправленную передачу ин- формационных кадров (т.е. кадров, содержащих пакеты) от од- ного агента к другому. В большинстве ситуаций пересылки данных между двумя агентами требуется двунаправленная передача, т.е. передача информационных кадров в обоих направлениях. В данном слу- чае каждый из агентов выступает как в роли отправителя, так и 273 в роли получателя. Протоколы, реализующие двунаправленную передачу, называются дуплексными протоколами. В дуплексных протоколах посылка подтверждений может быть совмещена с посылкой информационных кадров: если агент B успешно принял информационный кадр f от агента A, он может послать своё подтверждение получения кадра f не отдельным кадром, а в составе своего информационного кадра. Ниже мы излагаем примеры некоторых дуплексных протоко- лов. 8.4.7 Дуплексный протокол с чередующимися битами Простейшим дуплексным протоколом является излагаемый в этом параграфе дуплексный протокол с чередующимися бита- ми. Данный протокол является обобщением протокола ABP. В этом протоколе тоже участвуют два агента, но, в отличие от протокола ABP, поведение каждого из агентов описывается одним и тем же процессом, который совмещает в себе процессы отправителя и получателя из протокола ABP. Каждый кадр f , пересылаемый каким-либо из этих агентов, содержит пакет x и два бита: s и r, где • s имеет тот же смысл, что и в протоколе ABP: это бит, сопоставленный пакету x, • r является битом подтверждения последнего полученного неискажённого кадра. Для формирования кадров используется функция ϕ. Для извле- чения пакетов и битов из кадров используются функции info, seq и ack, обладающие следующими свойствами: info(ϕ(x, s, r)) = x seq(ϕ(x, s, r)) = s ack (ϕ(x, s, r)) = r Также агенты используют функцию inv для инвертирования значений битовых переменных. 274 С каждым из агентов связан свой таймер, поведение которо- го описывается процессом T imer, представленным диаграммой (8.21). Потоковый граф этого протокола имеет следующий вид: e u u e u e e u e u e u e u u e ? 6 start 1 timeout 1 e u u e ? 6 start 2 timeout 2 C 1 C 1 C 2 C 2 ' & $ % Channel ' & $ % Agent 1 T imer 1 T imer 2 ' & $ % Agent 2 - - In 1 Out 1 In 2 Out 2 (8.31) Процесс, описывающий поведение каждого из агентов, пред- ставляется в виде следующей блок-схемы: ' & $ % start s, r = 0 - ? In ? x ? C ! ϕ(x, s, 1 − r) ? start ! ? timeout ? C ? f - inv(s) seq(f ) = r 6 - ack(f ) = s f = ∗ 6 - 6 6 6 6 Out ! info(f ) inv(r) + − + + − − 275 Блок-схема, описывающая поведение конкретного агента, по- лучается из этой блок-схемы приписыванием соответствующего индекса к переменным и именам, входящим в эту блок-схему. Поведение канала представляется процессом (8.29), к которо- му применено переименование [ C 1 /S, C 2 /R ] Таким образом, каждый агент в этом протоколе посылает свой следующий пакет только после получения подтверждения своего предыдущего пакета. Нормальную работу данного протокола можно изобразить следующей диаграммой: Agent 1 - ϕ(x 0 ,0,1) Agent 2 - x 0 СУ 2 СУ 1 y 0 Agent 1 ϕ(y 0 ,0,0) Agent 2 Agent 1 - ϕ(x 1 ,1,0) Agent 2 - x 1 СУ 2 СУ 1 y 1 Agent 1 ϕ(y 1 ,1,1) Agent 2 Agent 1 - ϕ(x 2 ,0,1) Agent 2 - x 2 СУ 2 СУ 1 y 2 Agent 1 ϕ(y 2 ,0,0) Agent 2 Однако, если оба агента одновременно вышлют друг другу начальные кадры, то работа протокола будет не вполне нормаль- ной (хотя, тем не менее, передача пакетов в данном случае яв- ляется корректной), и может быть изображена следующей диа- 276 граммой: Agent 1 H H H H H j ϕ(x 0 ,0,1) ϕ(y 0 ,0,1) Agent 2 СУ 1 y 0 Agent 1 Agent 2 - x 0 СУ 2 Agent 1 H H H H H j ϕ(x 0 ,0,0) ϕ(y 0 ,0,0) Agent 2 Agent 1 Agent 2 Agent 1 H H H H H j ϕ(x 1 ,1,0) ϕ(y 1 ,1,0) Agent 2 СУ 1 y 1 Agent 1 Agent 2 - x 1 СУ 2 Agent 1 H H H H H j ϕ(x 1 ,1,1) ϕ(y 1 ,1,1) Agent 2 Agent 1 Agent 2 (8.32) Читателю предлагается самостоятельно • – определить процесс Spec, являющийся спецификацией этого протокола, и – доказать соответствие этого протокола спецификации Spec, • – модифицировать определённый в этом параграфе про- токол таким образом, чтобы при любом варианте рабо- ты модифицированного протокола не возникало ано- мальных эффектов, аналогичных приведённому выше (8.32), и – доказать корректность (т.е. соответствие специфика- ции Spec) модифицированного протокола. 8.4.8 Двунаправленная конвейерная передача Дуплексный протокол с чередующимися битами является прак- тически приемлемым только в том случае, когда длительность пересылки кадров по каналу пренебрежимо мала. 277 Если же время прохождения кадра по каналу большое, то лучше использовать конвейерную передачу, при которой от- правитель может послать несколько кадров подряд, не дожи- даясь подтверждений. Ниже мы рассматриваем два протокола двунаправленной конвейерной передачи, называемые протоко- лами скользящего окна (ПСО) (sliding window). Данные протоколы являются развитием дуплексного прото- кола с чередующимися битами, изложенного в параграфе 8.4.7. В этих протоколах • тоже участвуют два агента, поведение каждого из которых описывается одним и тем же процессом, совмещающим в себе функции отправителя и получателя, • аналогом бита, связанного с передаваемым кадром, явля- ется элемент множества вычетов Z n = {0, . . . , n − 1}, где n – некоторое фиксированное число вида 2 k Элемент множества Z n , связанный с кадром, называется но- мером этого кадра. Отметим, что номер кадра и порядковый номер кадра – это разные понятия: порядковые номера уникаль- ны, а номера циклически повторяются. 8.4.9 Протокол скользящего окна с возвратом Первый из рассматриваемых нами ПСО называется ПСО с воз- вратом (или ПСО с повторной передачей). Процесс, описывающий поведение агента этого ПСО, содер- жит среди своих переменных массив x[n], в компонентах которо- го могут содержаться отправленные, но ещё не подтверждённые пакеты. Совокупность компонентов массива x, в которых содер- жатся такие пакеты в текущий момент времени, называется ок- ном. С окном связаны три переменные этого процесса: • b – нижняя граница окна, • s – верхняя граница окна, и • w – количество пакетов в окне. 278 Значения переменных b, s и w принадлежат множеству Z n В начальный момент времени окно является пустым, и зна- чения переменных b, s и w равны 0. Добавление нового пакета к окну происходит путём выполне- ния следующих операций: • данный пакет записывается в компоненту x[s], и число s считается номером этого пакета • верхняя граница окна s увеличивается на 1 по модулю n, т.е. новое значение s полагается равным – s + 1, если s < n − 1, и – 0, если s = n − 1, • количество пакетов в окне w увеличивается на 1. Удаление пакета из окна происходит следующим образом: • нижняя граница окна b увеличивается на 1 по модулю n, и • количество пакетов в окне w уменьшается на 1 т.е. удаляется тот пакет, номер которого равен нижней границе окна. Для упрощения понимания операций работы с окном можно использовать следующую образную аналогию: • совокупность компонентов массива x можно рассматривать как “свёрнутую в кольцо” (после компоненты x[n − 1] идёт компонента x[0]) • в каждый момент времени окно представляет собой связное подмножество этого кольца, • во время работы процесса окно перемещается по этому коль- цу в одном и том же направлении. Если окно достигает максимального размера (n − 1), то агент не принимает новые пакеты от своего СУ до тех пор, пока раз- мер окна не уменьшится. Возможность приёма новых пакетов определяется булевой переменной enable: если её значение равно 279 1, то агент может принимать новые пакеты от своего СУ, а если 0, то не может. Когда агент получает подтверждение пакета, номер которого равен нижней границе окна, этот пакет удаляется из окна. С каждой компонентой массива x связан таймер, при помощи которого определяется время ожидания подтверждения полу- чения пакета, содержащегося в этой компоненте. Совокупность всех этих таймеров рассматривается как один процесс T imers, который имеет массив t [n] булевых переменных. Данный про- цесс определяется следующим образом: Init = (t = (0, . . . , 0)) 6 stop ? i t [i] := 0 - start ? i t [i] := 1 |