Введение в распределённые алгоритмы. Ж. Тель (2009) (не распознанно) (1185664), страница 30
Текст из файла (страница 30)
Формула P1 является инвариантом протокола с таймерами.Д о к а з а т е л ь с т в о. Прежде всего заметим, что, как только предикатOk(i) становится истинным для некоторого i, он больше никогда не может статьложным. Вначале нет никакого соединения, нет пакетов и B = 0, вследствие чеговыполняется утверждение P1 .Ap : Действие Ap может открыть сеанс связи, но выполнимость соотношения(10) при этом сохраняется, потому что при открытии сеанса связи Low = 0 и ∀i << B : Ok(i) вследствие выполнимости соотношения (9).Sp : Действие Sp может отправить пакет hdata, s, I, w, i, но, ввиду того чтоs имеет значение true только в том случае, когда I = Low, выполнимость соотношения (10) приводит к тому, что выполнимость соотношения (11) сохраняется.Rp : Значение переменной Low может увеличиться, если будет получен пакетhack, I, i.
Тем не менее выполнимость соотношения (10) сохраняется, посколькув случае получения этого подтверждения будет выполняться соотношению (13)∀i < B + I : Ok(i).Ep : Значение переменной Low может увеличиться, когда выполняется действие Ep , но формирование сообщения об ошибке приводит к тому, что выполнимость соотношения (10) сохраняется.Д о к а з а т е л ь с т в о. В самом начале соединения отсутствуют, нет никаких пакетов, B = 0, и поэтому утверждение P0 является истинным.Ap : Выполнимость соотношения (1) сохраняется, поскольку оператор присваивания, в правой части которого стоит St, всегда приводит к тому, что выполняется равенство St = S.
Выполнимость соотношения (3) сохраняется, потому что, перед тем как переменная High увеличит свое значение, элементуUt [B + High] присваивается значение U. Выполнимость соотношений (5), (6)и (7) сохраняется, поскольку значение St может только увеличиться. Выполнимость соотношения (8) сохраняется, поскольку значение High может толькоувеличиться.Sp : Выполнимость соотношения (1) сохраняется, поскольку St всегда будетприсвоено значение S.
Выполнимость соотношения (4) сохраняется, потому чтокаждый отправляемый пакет имеет время оставшейся жизни, равное . Выполнимость соотношения (5) сохраняется, так как пакет h.., i отправлен, St полагается равным S и S = R + 2 . Выполнимость соотношений (6) и (7) сохраняется, поскольку рассматриваемое действие может только увеличить значение St.Соотношение (8) сохраняется, так как для нового пакета выполняются условияw = inp [B + i] и i < High.Rp : Действие Rp не изменяет значений ни одной из переменных, фигурирующих в формуле P0 , и изъятие пакета сохраняет соотношения (4) и (7).Ep : Действие Ep не изменяет значений ни одной из переменных, фигурирующих в формуле P0 .Cp : Действие Cp может нарушить справедливость заключений в соотношениях (5), (6) и (7), но (согласно соотношениям (2), (5), (6) и (7)) оно применимотолько тогда, когда предпосылки этих соотношений не выполняются. ДействиеCp также изменяет значение переменной B, но, поскольку согласно соотношениям (5) и (7) ни один пакет не находится на этапе пересылки, выполнимостьсоотношения (8) сохраняется.Rq : Выполнимость соотношения (2) сохраняется, так как переменной Rt всегда присваивается значение R (если присваивание имеет место).
Выполнимостьсоотношения (6) сохраняется, поскольку переменной Rt присваивается значение R только при получении пакета hdata, s, i, w, i, а из соотношений (4) и (5)следует, что в этом случае выполняется формула cs ∧ St > R + .Sq : Выполнимость соотношения (4) сохраняется, потому что при отправлении каждого пакета оставшееся время его жизни полагается равным . Выполнимость соотношения (7) сохраняется, поскольку при отправлении пакета hack, i, iв случае, когда cr имеет значение true, выполняется равенство = , и поэтомуиз соотношений (2) и (6) следует неравенство St > .Loss: Выполнимость соотношений (4), (5), (7) и (8) сохраняется, потому чтоизъятие пакета может привести лишь к тому, что нарушатся предпосылки этихсоотношений.Dupl: Выполнимость соотношений (4), (5), (7) и (8) сохраняется, так как дублирующая вставка пакета m возможна только тогда, когда пакет m уже содержится в канале; отсюда вытекает, что следствия соответствующих соотношенийбыли выполнены уже перед самой вставкой.106Гл.
3. Коммуникационные протоколы3.2. Протокол с таймерамиСделав дополнительное допущение, мы можем доказать теперь первую частьспецификации протокола. Без этого допущения отправитель может оказаться чересчур «ленивым» при составлении отчета о потерянных словах; в алгоритме 3.4всего лишь указано, что сообщение о потере не может быть сформировано втечение 2 + R единиц времени, следующих за окончанием интервала отправленияслова, но там не сказано о том, что это сообщение рано или поздно обязано бытьсформировано. Поэтому давайте сделаем дополнительное допущение о том, чтодействие Ep рано или поздно будет выполнено процессом p в разумные сроки,скажем, не позднее Ut [B + Low] = −2 − R − .Теорема 3.12 (отсутствие потерь). Каждое слово массива inp либо достигает процесса q, либо отмечается процессом p как утраченное в течение U + 2 + R + единиц времени после поступления этого слова процессу p.109Д о к а з а т е л ь с т в о.
При поступлении слова inp [I] выполняется неравенство B + High > I, и оно продолжает выполняться далее. Если сеанс связи закрывается спустя предписанный период времени после поступления словаinp [I] , значит, B > I, и утверждение теоремы следует из соотношения (9). Еслиспустя указанный период времени сеанс связи остается открытым и B + Low 6 I,все слова, порядковые номера которых располагаются на отрезке B + Low..I,будут отмечены в отчете спустя 2 + R единиц времени по окончании интервалавремени, отведенного для отправления слова in p [I] . Отсюда следует, что записьв отчете будет сделана спустя 2 + R + единиц времени после окончания срока,отведенного для отправления сообщения, т. е. спустя U +2 +R+ единиц временипосле поступления слова.
Это также влечет за собой выполнимость неравенстваI < B + Low, и поэтому рассматриваемое слово будет либо отмечено в отчете,либо доставлено по назначению согласно соотношению (10).Чтобы установить второе требование корректности протокола, необходимопоказать, что каждое слово, которое было вручено потребителю, имеет большийпорядковый номер (в массиве inp), чем ранее врученное слово. Воспользуемся записью pr для обозначения порядкового номера самого последнего из врученных потребителю слов (для удобства будем полагать, что вначале pr = −1и Ut [−1] = −∞). Рассмотрим формулу P2 , имеющую следующий вид:∧∧∧∧∧P1hdata, s, i, w, i ∈ Mq =⇒ Ut [B + i] > −i1 6 i2 < B + High =⇒ Ut [i1 ] 6 Ut [i2 ]cr =⇒ Rt > Ut [pr] +pr < B + High ∧ (Ut [pr] > − =⇒ cr)cr =⇒ B + Exp = pr + 1 ∧P2 ≡(14)(15)(16)(17)(18)Лемма 3.13.
Формула P2 является инвариантом протокола с таймерами.Д о к а з а т е л ь с т в о. Первоначально мультимножество M q пусто, B+Highравно нулю, выполняются соотношения ¬cr и Ut [pr] < − ; отсюда следует выполнимость соотношений (14) – (18).Ap : Выполнимость соотношения (15) сохраняется, потому что только что доставленное слово сопровождается таймером U, показание которого согласно соотношению (3) по крайней мере равно показанию таймеров, сопровождающихранее доставленные слова.Sp : Выполнимость соотношения (14) сохраняется, так как Ut [B + i] > 0, и приотправлении пакета соблюдается равенство = .Cp : Выполнимость соотношений (14), (16) и (18) сохраняется, поскольку согласно соотношениям (5) и (6) предпосылки этих соотношений неверны, когдаприменимо действие Cp .
Выполнимость соотношения (15) сохраняется, потомучто переменной B присвоено значение B + High и показания таймеров не изменились. Выполнимость соотношения (17) сохраняется, ввиду того, что переменнойB присвоено значение B + High, а значения pr и cr не изменяются.Cp : Действие Cp приводит к тому, что cs получает значение false, но это действие применимо только тогда, когда St < 0 и Low = High.
Из соотношения(10) следует, что неравенство ∀i < B + High : Ok(i) соблюдается в момент выполнения действия Cp , и поэтому выполнимость соотношения (9) сохраняется.В результате выполнения этого действия предпосылка соотношения (10) становится ложной, и поэтому из соотношений (5), (6) и (7) следует, что и предпосылкисоотношений (11), (12) и (13) также становятся ложными; отсюда следует, чтовыполнимость соотношений (10), (11), (12) и (13) сохраняется.Rq : Вначале рассмотрим случай, когда процесс q получает пакет hdata, true, I, w, i,в то время как никакого соединения нет (cr имеет значение false). Тогда согласносоотношению (11) имеет место неравенство ∀i < B + I : Ok(i), и в результате этого действия будет доставлено слово w. Коль скоро согласно соотношению(8) верно равенство w = inp [B + I] , в результате присваивания Exp := I + 1выполнимость соотношения (12) сохраняется.Теперь обратимся к случаю, когда значение Exp увеличивается в результатеполучения пакета hdata, s, Exp, w, i при открытом сеансе связи.
Как следует изсоотношения (12), перед получением сообщения справедливо неравенство ∀i << B + Exp : Ok(i) и в ходе осуществления рассматриваемого действия будетполучено слово w = inp [B + Exp] . Следовательно, при увеличении значения Expвыполнимость соотношения (12) сохраняется.Sq : Как следует из соотношения (12), при отправлении сообщения hack, Exp,выполнимость соотношения (13) сохраняется.Loss: Применение действия Loss приводит к тому, что предпосылки всех соотношений становятся ложными.Dupl: Дублирующая вставка пакета m может осуществиться только в томслучае, когда предпосылки соответствующих соотношений (а значит, и их следствия) были верны перед этой вставкой.Time: В соотношениях (9) – (13) никакие таймеры не фигурируют. Изъятиепакета или закрытие сеанса связи процессом q может лишь сделать ложнымипредпосылки соотношений (11), (12) или (13).108110Гл. 3.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
