Введение в распределённые алгоритмы. Ж. Тель (2009) (не распознанно) (1185664), страница 31
Текст из файла (страница 31)
Коммуникационные протоколы3.2. Протокол с таймерами1113.2.3. Обсуждение протоколаRq : Выполнимость соотношения (16) сохраняется, так как в том случае, когдапеременной Rt присвоено значение R (после того как доставлено слово), неравенство Ut [pr] 6 U соблюдается вследствие соотношения (3) и при этом имеетместо неравенство R > 2 + U. Выполнимость соотношения (17) сохраняется,поскольку неравенство pr < B + High следует из (8) и при этом cr принимаетзначение true. Выполнимость соотношения (18) сохраняется, так как значениеExp становится равным i + 1, а значение pr становится равным B + i; отсюдаследует, что соотношение (18) становится истинным.Time: Выполнимость соотношения (14) сохраняется, ввиду того что значенияUt [B + i] и уменьшаются на одну и ту же величину (а изъятие пакета можетлишь сделать ложным предпосылку соотношения).
Выполнимость соотношения(15) сохраняется, ввиду того что значения Ut [i 1 ] и Ut [i2 ] уменьшаются на однуи ту же величину. Выполнимость соотношения (16) сохраняется, потому что этодействие не обращает cr в истину и значения Rt и Ut [pr] уменьшаются на одну и ту же величину. Выполнимость соотношения (17) сохраняется, посколькуего заключение может стать ложным только тогда, когда значение Rt становится не большим нуля, а это, согласно соотношению (16), означает, что значениеUt [pr] не превосходит − .
Выполнимость соотношения (18) сохраняется, поскольку в том случае, когда cr не обращается в ложь, значения B, Exp и pr неизменяются.Действия Rp , Ep и Sq не изменяют значений тех переменных, которые фигурируют в соотношениях (14) – (18). Действия Loss и Dupl сохраняют выполнимостьсоотношений (14) – (18); обоснование этого проводится так же, как и в предыдущих доказательствах.Некоторые расширенные варианты рассмотренного протокола уже обсуждались во введении к этому параграфу. В заключение мы продолжим обсуждениепротокола, а также тех методов, которые были введены и использованы в этомпараграфе.Качественный анализ протокола.
Требования отсутствия потерь и упорядочения являются свойствами безопасности, и для того чтобы удовлетворитьэти требования, можно предложить чрезвычайно простое решение, а именно, протокол, который вообще не отправляет и не принимает ни одного пакета, а каждоеслово заносит в отчет как утраченное. Нет нужды объяснять, почему такой протокол, который не обеспечивает передачи данных от отправителя к получателю,нельзя считать очень «хорошим» решением.Хорошим считается такое решение, которое не только удовлетворяет требованиям отсутствия потерь и упорядочения, но также сообщает об утратекак можно меньшего числа слов.
Чтобы достичь этой цели мы должны снабдитьпротокол, описанный в этом параграфе, некоторым механизмом, который позволял бы отправлять каждое слово повторно (на протяжении интервала отправления слова), до тех пор пока не будет получено подтверждение о его доставке.Интервал отправления должен быть достаточно протяженным, чтобы позволитьосуществлять многократную передачу определенных слов и сделать тем самымвероятность утраты слова как можно меньшей.Со стороны получателя должен срабатывать механизм, который запускаетотправление подтверждающих сообщений при доставке пакета или его получениипри открытом сеансе связи.Лемма 3.14. Из формулы P2 следует соотношениеОграниченные порядковые номера. Порядковые номера, используемые в протоколе, можно ограничить, доказав для этого протокола утверждение, аналогичное лемме 3.9 для симметричного протокола раздвижного окна [187, § 3.2] .
Дляэтого необходимо ввести допущение о том, что скорость поступления слов навход процесса p ограничена таким образом, чтобы очередное слово поступалоспустя не менее U + 2 + R единиц времени после поступления L-го по порядку предшествующего слова. Чтобы достичь этого, действие A p нужно снабдитьпредохранителемhdata, s, i1 , w, i ∈ Mq =⇒ (cr ∨ B + i1 > pr).Д о к а з а т е л ь с т в о. Согласно соотношению (14) из условия hdata, s, i 1 , w, i∈∈ Mq следует, что Ut [B + i1 ] > − > − . Если B + i1 6 pr, то, принимая во внимание, что согласно соотношению (15) справедливо неравенство pr < B + High,получаем неравенство Ut [pr] > − , из которого на основании соотношения (17)следует истинность предиката cr.{ (High < L) ∨ (Ut [B + High − L] < −R − 2 ) }.Теорема 3.15 (упорядочение). Слова, доставленные процессом q потребителю, расположены в строго возрастающем порядке в массиве inp .Д о к а з а т е л ь с т в о.
Предположим, что процесс q получает пакет hdata, s, i 1 , w, iи вручает потребителю слово w. Если перед получением не было никакого соединения, то B + i1 > pr (по лемме 3.14), и поэтому слово w в массиве inpрасполагалось в позиции, номер которой следует за pr. Если же соединение имелось, то i1 = Exp, и поэтому согласно соотношению (18) имеют место равенстваB + i1 = B + Exp = pr + 1, из которых следует, что w = inp [pr + 1] .В рамках такого допущения можно показать, что порядковые номера полученных пакетов данных отстоят не более чем на 2L от ожидаемого номера Exp,а порядковые номера в подтверждающих сообщениях отстоят не более чем на Lот номера High. Следовательно, при передаче увеличение порядковых номеровможно проводить по модулю 2L.Облик действий и инвариантов.
Теоретико-доказательный подход сводитанализ коммуникационного протокола к задаче проверки и преобразования формул (иногда весьма громоздких). Манипуляции с формулами — это очень «на-Гл. 3. Коммуникационные протоколы3.2. Протокол с таймерами*)00:= . . . ; (*0000endАлгоритм 3.8. Модифицированное действие Timeили 10−6 .) Такое поведение таймеров моделируется действием Time- , котороеописано алгоритмом 3.8.Как уже отмечалось ранее, действие Time сохраняет выполнимость предложений вида Xt > Yt + C, потому что значения таймеров в обеих частях неравенствауменьшаются на одну и ту же величину, и неравенство Xt > Yt + C влечет соотношение (Xt − ) > (Yt − ) + C.
Аналогичное замечание относится и к действиюTime- . Для действительных чисел Xt, Yt, , 0 , 00 , r и c, удовлетворяющих неравенствам > 0 и r > 1, соотношение[Xt > r2 Yt + c] ∧6 0 6 ×r ∧6 00 6 × rгде Xt и Yt — таймеры, а C — константа.Неточные таймеры. Действие Time моделирует идеальные таймеры, значения которых уменьшается в точности на по истечении единиц времени, нона практике таймеры подвержены неточностям, которые называются расхождениями. Обычно предполагается, что это расхождение является -ограниченнымдля некоторой известной константы . Это означает, что за период времени длиныпоказания таймера уменьшаются на величину 0 , которая удовлетворяет неравенству / (1 + ) 6 0 6 × (1 + ).
(Обычно является величиной порядка 10 −5rr(Xt − 0) > r2 (Yt −влечет неравенствоПредложения такого вида могут утратить истинность в случае потери или дублирования пакетов, и поэтому их нельзя использовать при доказательстве корректности алгоритмов, от которых требуется устойчивость по отношению к подобнымсбоям.Аналогичное замечание касается устройства инвариантов, относящихся к действию Time. Как уже говорилось, это действие сохраняет выполнимость всехпредложений видаXt > Yt + C,предусловие =⇒ ∃m ∈ M : A(m).или*)66 × (1 + ) *)(1 + );Rt := Rt −if Rt 6 0 then delete (Rt, Exp) ;(* Поля вычисляются точно *)forall h.., i ∈ Mp , Mq dobegin := − ;if 6 0 then remove packetend00m∈M:= . .
. ; (*0и, как нетрудно убедиться, выполнимость соотношений такого вида сохраняетсяпри дублировании или потере пакетов. В последующих главах мы будем рассматривать инварианты более общего вида, напримерXf(m) = K6 6 × (1 + ) *)(1 + )forall i do Ut [i] := Ut [i] − 0 ;St := St − 0 ;(* Значения всех таймеров процесса q уменьшаются на00∀m ∈ M : A(m),Time- : { > 0 }begin (* Значения всех таймеров процесса p уменьшаются надежный» прием, потому что на каждом шаге можно провести очень тщательнуюпроверку и вероятность ошибки чрезвычайно мала.
И все же есть определенныйриск того, что при этом может быть потеряно общее понимание протокола и егосвязь с рассматриваемыми формулами. Вопрос об устройстве протокола можно осмыслить как с прагматической, так и с формальной точки зрения. Флетчер и Ватсон в работе [85] настаивают на том, что управляющая информациядолжна быть «защищена», имея в виду, что ее смысл не должен изменяться приутрате или дублировании пакетов; такова прагматическая точка зрения. При использовании теоретико-доказательного подхода к решению задачи верификации«смысл» управляющей информации проявляется в выборе тех или иных утверждений в качестве инвариантов. Формальный взгляд на устройство протоколаопределяется выбором этих инвариантов и устройством переходов, сохраняющихэти инварианты.
На самом деле, как будет показано далее, замечание Флетчераи Ватсона можно переформулировать в терминах описания структуры формул,которые разрешается или не разрешается использовать в качестве инвариантовпротокола, стойкого по отношению к потерям и дублированию пакетов.Все соотношения (дизъюнкты), входящие в состав формулы P 2 и касающиесяпакетов, имеют следующий общий вид:11311200) + c.Следовательно, действие Time- сохраняет выполнимость предложений видаXt > (1 + ) 2 Yt + c.Наш протокол теперь можно так модифицировать, чтобы он мог работатьс расходящимися таймерами; инварианты при этом преобразуются соответствующим образом.
Для того чтобы другие действия также сохраняли выполнимостьмодифицированных инвариантов, константы R и S, используемые в протоколе,должны удовлетворять соотношениямR > (1 + ) ((1 + )U + (1 + ) 2 ) и S > (1 + ) (2 + (1 + )R).В остальном, за исключением указанных констант, протокол остается без изменений. Его инвариант представлен на рис. 3.9.Гл. 3. Коммуникационные протоколы3.3. Упражнения к главе 3cs =⇒ St 6 Scr =⇒ 0 < Rt 6 R∀ i < B + High : Ut [i] 6 U∀ h. .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
