Введение в распределённые алгоритмы. Ж. Тель (2009) (1185665), страница 30
Текст из файла (страница 30)
Формула Ро является инвариантом протокола с таймерами.Слова первогосеанса связиСлова второгосеанса связиИндексация слов в протоколе:Текущий сеанс связиВВ + LowВ + H igh}А.г|ОКНО[отправ.п тОРис. 3.7. Порядковые номера словLowH igh106Гл. 3. Коммуникационные протоколыД о к а з а т е л ь с т в о . В самом начале соединения отсутствуют, нет никаких пакетов, В = 0, и поэтому утверждение Ро является истинным.Ар: Выполнимость соотношения (1) сохраняется, поскольку оператор присваивания, в правой части которого стоит S t , всегда приводит к тому, что выполняется равенство S t = S . Выполнимость соотношения (3) сохраняется, потому что, перед тем как переменная High увеличит свое значение, элементуU t[ B + High ] присваивается значение U .
Выполнимость соотношений (5), (6)и (7) сохраняется, поскольку значение S t может только увеличиться. Выполнимость соотношения (8) сохраняется, поскольку значение High может толькоувеличиться.Sp: Выполнимость соотношения (1) сохраняется, поскольку S t всегда будетприсвоено значение 5. Выполнимость соотношения (4) сохраняется, потому чтокаждый отправляемый пакет имеет время оставшейся жизни, равное ц. Выполнимость соотношения (5) сохраняется, так как пакет (.., ц) отправлен, S t полагается равным S и S = R + 2ц.
Выполнимость соотношений (6) и (7) сохраняется, поскольку рассматриваемое действие может только увеличить значение S t .Соотношение (8) сохраняется, так как для нового пакета выполняются условияw = itip \В + /] и / < High.R^,: Действие Rp не изменяет значений ни одной из переменных, фигурирующих в формуле Р0, и изъятие пакета сохраняет соотношения (4) и (7).Ер\ Действие Ер не изменяет значений ни одной из переменных, фигурирующих в формуле Pq.Ср: Действие Ср может нарушить справедливость заключений в соотношениях (5), (6) и (7), но (согласно соотношениям (2), (5), (6) и (7)) оно применимотолько тогда, когда предпосылки этих соотношений не выполняются.
ДействиеСр также изменяет значение переменной В, но, поскольку согласно соотношениям (5) и (7) ни один пакет не находится на этапе пересылки, выполнимостьсоотношения (8) сохраняется.R9: Выполнимость соотношения (2) сохраняется, так как переменной Rt всегда присваивается значение R (если присваивание имеет место).
Выполнимостьсоотношения (6) сохраняется, поскольку переменной Rt присваивается значение R только при получении пакета (data, s, i, w, р), а из соотношений (4) и (5)следует, что в этом случае выполняется формула cs А 5 / > R + ц.S4: Выполнимость соотношения (4) сохраняется, потому что при отправлении каждого пакета оставшееся время его жизни полагается равным ц. Выполнимость соотношения (7) сохраняется, поскольку при отправлении пакета (аск, г, р)в случае, когда сг имеет значение true, выполняется равенство р = ц, и поэтомуиз соотношений (2) и (6) следует неравенство St > ц.Loss: Выполнимость соотношений (4), (5), (7) и (8) сохраняется, потому чтоизъятие пакета может привести лишь к тому, что нарушатся предпосылки этихсоотношений.Dupl: Выполнимость соотношений (4), (5), (7) и (8) сохраняется, так как дублирующая вставка пакета т возможна только тогда, когда пакет т уже содержится в канале; отсюда вытекает, что следствия соответствующих соотношенийбыли выполнены уже перед самой вставкой.1073.2.
Протокол с таймерамиTime: Выполнимость соотношений (1), (2) и (3) сохраняется, поскольку значения переменных St, Rt и Ut[i\ могут лишь уменьшиться и сеанс связи получателя закрывается, когда значение Rt становится равным 0. Выполнимостьсоотношения (4) сохраняется, потому что значение р может лишь уменьшитьсяи пакет изымается, когда значение его поля р становится равным 0.
Заметим,что действие Time приводит к уменьшению значения всех таймеров (включая те,которые содержатся в поле р пакетов) на одну и ту же величину; поэтомусохраняется выполнимость всех соотношений вида Xt > Yt + С, где Xt и Yt —таймеры, а С — константа. Это означает, что соотношения (5), (6) и (7) остаютсяверными.□Первое требование, которое предъявляется к рассматриваемому протоколу,состоит в том, что каждое слово должно быть рано или поздно доставлено поназначению или занесено в отчет как утраченное. Определим предикат Ok{i) следующей формулой:Ok(i) -^=^> error[i] = true Vпроцессу q было доставлено сообщение inp[i\.Как будет показано, протокол не теряет ни одного слова, не отметив этого факта.Рассмотрим формулу Р\ следующего вида:Pi=ЛЛЛЛЛРо-1 cs ==>- V/ < В: Ok(i)cs =*> V/ < В + Low: Ok(i)(data, true, /, да, р) € Mq = > V/ < В + /: Ok{i)сг =*- V/ < B + Exp: Ok{i)(ack, I,р) е М р ==> V/ < В + /: Ok(i)(9)(10)(11)(12)(13)Лемма 3.11.
Формула Р\ является инвариантом протокола с таймерами.Д о к а з а т е л ь с т в о . Прежде всего заметим, что, как только предикатOk{i) становится истинным для некоторого /, он больше никогда не может статьложным. Вначале нет никакого соединения, нет пакетов и В = 0, вследствие чеговыполняется утверждение Р \.Ар: Действие Ар может открыть сеанс связи, но выполнимость соотношения(10) при этом сохраняется, потому что при открытии сеанса связи Low = 0 и V/ << В : Ok{i) вследствие выполнимости соотношения (9).Sp: Действие Sp может отправить пакет (data, s, /, да, р), но, ввиду того чтоs имеет значение true только в том случае, когда / = Low, выполнимость соотношения (10) приводит к тому, что выполнимость соотношения (11) сохраняется.Rp: Значение переменной Low может увеличиться, если будет получен пакет(ack, I, р). Тем не менее выполнимость соотношения (10) сохраняется, посколькув случае получения этого подтверждения будет выполняться соотношению (13)V/ < В + I : Ok(i).Ер\ Значение переменной Low может увеличиться, когда выполняется действие Ер , но формирование сообщения об ошибке приводит к тому, что выполнимость соотношения (10) сохраняется.108Гл.
3. Коммуникационные протоколыСр: Действие Ср приводит к тому, что cs получает значение false, но это действие применимо только тогда, когда St < 0 и Low = High. Из соотношения(10) следует, что неравенство Vi < В + High : Ok(i) соблюдается в момент выполнения действия Ср, и поэтому выполнимость соотношения (9) сохраняется.В результате выполнения этого действия предпосылка соотношения (10) становится ложной, и поэтому из соотношений (5), (6) и (7) следует, что и предпосылкисоотношений (11), (12) и (13) также становятся ложными; отсюда следует, чтовыполнимость соотношений (10), (11), (12) и (13) сохраняется.R^: Вначале рассмотрим случай, когда процесс q получает пакет (data, true, I, w, p),в то время как никакого соединения нет (сг имеет значение false).
Тогда согласносоотношению (11) имеет место неравенство V/ < В + I : Ok{i), и в результате этого действия будет доставлено слово да. Коль скоро согласно соотношению(8) верно равенство да = inp[B + /], в результате присваивания Exp := I + 1выполнимость соотношения (12) сохраняется.Теперь обратимся к случаю, когда значение Ехр увеличивается в результатеполучения пакета (data, s, Ехр, да, р) при открытом сеансе связи. Как следует изсоотношения (12), перед получением сообщения справедливо неравенство Vi << В + Ехр : Ok(i) и в ходе осуществления рассматриваемого действия будетполучено слово да = inp[B + Ехр].
Следовательно, при увеличении значения Ехрвыполнимость соотношения (12) сохраняется.Sq: Как следует из соотношения (12), при отправлении сообщения (аск, Ехр, рвыполнимость соотношения (13) сохраняется.Loss: Применение действия Loss приводит к тому, что предпосылки всех соотношений становятся ложными.Dupl: Дублирующая вставка пакета т может осуществиться только в томслучае, когда предпосылки соответствующих соотношений (а значит, и их следствия) были верны перед этой вставкой.Time: В соотношениях (9)—(13) никакие таймеры не фигурируют.
Изъятиепакета или закрытие сеанса связи процессом q может лишь сделать ложнымипредпосылки соотношений (11), (12) или (13).□Сделав дополнительное допущение, мы можем доказать теперь первую частьспецификации протокола. Без этого допущения отправитель может оказаться чересчур «ленивым» при составлении отчета о потерянных словах; в алгоритме 3.4всего лишь указано, что сообщение о потере не может быть сформировано втечение 2[i+R единиц времени, следующих за окончанием интервала отправленияслова, но там не сказано о том, что это сообщение рано или поздно обязано бытьсформировано.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
