Введение в распределённые алгоритмы. Ж. Тель (2009) (1185665), страница 31
Текст из файла (страница 31)
Поэтому давайте сделаем дополнительное допущение о том, чтодействие Ер рано или поздно будет выполнено процессом р в разумные сроки,скажем, не позднее Ut[B + Low] = —2р - R - X.Теорема 3.12 (отсутствие потерь). Каждое слово массива inp либо достигает процесса q, либо отмечается процессом р как утраченное в течение U + 2р + R + X единиц времени после поступления этого слова процессу р.3.2. Протокол с таймерами109Д о к а з а т е л ь с т в о . При поступлении слова inp[I] выполняется неравенство В + High > I, и оно продолжает выполняться далее.
Если сеанс связи закрывается спустя предписанный период времени после поступления словаinp\l\, значит, В > I, и утверждение теоремы следует из соотношения (9). Еслиспустя указанный период времени сеанс связи остается открытым и В + Low A Lвсе слова, порядковые номера которых располагаются на отрезке В + Low..!,будут отмечены в отчете спустя 2\i-\- R единиц времени по окончании интервалавремени, отведенного для отправления слова inp[I], Отсюда следует, что записьв отчете будет сделана спустя 2yL-\-R + X единиц времени после окончания срока,отведенного для отправления сообщения, т.
е. спустя U+2yi+R+'k единиц временипосле поступления слова. Это также влечет за собой выполнимость неравенства/ < В + Low, и поэтому рассматриваемое слово будет либо отмечено в отчете,либо доставлено по назначению согласно соотношению (10).□Чтобы установить второе требование корректности протокола, необходимопоказать, что каждое слово, которое было вручено потребителю, имеет большийпорядковый номер (в массиве in p), чем ранее врученное слово. Воспользуемся записью рг для обозначения порядкового номера самого последнего из врученных потребителю слов (для удобства будем полагать, что вначале рг = —1и Ut[—1] = —оо). Рассмотрим формулу Р2 , имеющую следующий вид:Р2=АААААЛ(data, s, i, w, p) € Mq =£• Ut[B + i] > p —Вh ^ h < В + High =^- Ut[i\] < Ut[i2]cr =$ - Rt A Ut[pr] + pрг < В + High A (Ut[pr] > - в ==► cr)cr =$ - В + Exp = pr + 1 A(14)(15)(16)(17)(18)Лемма 3.13.
Формула Р2 является инвариантом протокола с таймерами.Д о к а з а т е л ь с т в о . Первоначально мультимножество Mq пусто, B+Highравно нулю, выполняются соотношения ->сг и Ut[pr] < —pi; отсюда следует выполнимость соотношений (14)—(18).Ар: Выполнимость соотношения (15) сохраняется, потому что только что доставленное слово сопровождается таймером U, показание которого согласно соотношению (3) по крайней мере равно показанию таймеров, сопровождающихранее доставленные слова.Sp: Выполнимость соотношения (14) сохраняется, так как Ut[B+i\ > 0, и приотправлении пакета соблюдается равенство р = р.Ср: Выполнимость соотношений (14), (16) и (18) сохраняется, поскольку согласно соотношениям (5) и (6) предпосылки этих соотношений неверны, когдаприменимо действие Ср.
Выполнимость соотношения (15) сохраняется, потомучто переменной В присвоено значение В +High и показания таймеров не изменились. Выполнимость соотношения (17) сохраняется, ввиду того, что переменнойВ присвоено значение В + High, а значения рг и сг не изменяются.Гл. 3.
Коммуникационные протоколыпоR^: Выполнимость соотношения (16) сохраняется, так как в том случае, когдапеременной Rt присвоено значение R (после того как доставлено слово), неравенство Ut[pr] ^ U соблюдается вследствие соотношения (3) и при этом имеетместо неравенство R > 2pi + 1/. Выполнимость соотношения (17) сохраняется,поскольку неравенство рг < В + High следует из (8) и при этом сг принимаетзначение true. Выполнимость соотношения (18) сохраняется, так как значениеЕхр становится равным / + 1, а значение рг становится равным В + /; отсюдаследует, что соотношение (18) становится истинным.Time: Выполнимость соотношения (14) сохраняется, ввиду того что значенияUt[B + /] и р уменьшаются на одну и ту же величину (а изъятие пакета можетлишь сделать ложным предпосылку соотношения).
Выполнимость соотношения(15) сохраняется, ввиду того что значения Ut[i\ \ и Ut[i>\ уменьшаются на однуи ту же величину. Выполнимость соотношения (16) сохраняется, потому что этодействие не обращает сг в истину и значения Rt и Ut[pr] уменьшаются на одну и ту же величину. Выполнимость соотношения (17) сохраняется, посколькуего заключение может стать ложным только тогда, когда значение Rt становится не большим нуля, а это, согласно соотношению (16), означает, что значениеUt[pr] не превосходит —pi.
Выполнимость соотношения (18) сохраняется, поскольку в том случае, когда сг не обращается в ложь, значения В, Ехр и рг неизменяются.Действия Rp, Ер и Sq не изменяют значений тех переменных, которые фигурируют в соотношениях (14)—(18). Действия Loss и Dupl сохраняют выполнимостьсоотношений (14)—(18); обоснование этого проводится так же, как и в предыдущих доказательствах.□Лемма 3.14. Из формулы Рч следует соотношение{d a ta ,s, i\ , да, р) <Е Mq =*- (сг V В + i\ > рг).Д о к а з а т е л ь с т в о . Согласно соотношению (14) из условия (data, s ,i \ ,w€M q следует, что Ut[B+i{] > р —pi > —pi. Если B + i\ ^ рг, то, принимая во внимание, что согласно соотношению (15) справедливо неравенство рг < В + High,получаем неравенство Ut[pr] > —pi, из которого на основании соотношения (17)следует истинность предиката сг.□Теорема 3.15 (упорядочение). Слова, доставленные процессом q потребителю, расположены в строго возрастающем порядке в массиве inp.Д о к а з а т е л ь с т в о .
Предположим, что процесс q получает пакет (data, s,и вручает потребителю слово да. Если перед получением не было никакого соединения, то В + i\ > рг (по лемме 3.14), и поэтому слово да в массиве inpрасполагалось в позиции, номер которой следует за рг. Если же соединение имелось, то i\ = Ехр, и поэтому согласно соотношению (18) имеют место равенстваВ + /1 = В + Ехр = рг + 1, из которых следует, что да = inp [рг + 1].□3.2. Протокол с таймерами3.2.3. Обсуждение протоколаНекоторые расширенные варианты рассмотренного протокола уже обсуждались во введении к этому параграфу. В заключение мы продолжим обсуждениепротокола, а также тех методов, которые были введены и использованы в этомпараграфе.Качественный анализ протокола.
Требования отсутствия потерь и упорядочения являются свойствами безопасности, и для того чтобы удовлетворитьэти требования, можно предложить чрезвычайно простое решение, а именно, протокол, который вообще не отправляет и не принимает ни одного пакета, а каждоеслово заносит в отчет как утраченное. Нет нужды объяснять, почему такой протокол, который не обеспечивает передачи данных от отправителя к получателю,нельзя считать очень «хорошим» решением.Хорошим считается такое решение, которое не только удовлетворяет требованиям отсутствия потерь и упорядочения , но также сообщает об утратекак можно меньшего числа слов.
Чтобы достичь этой цели мы должны снабдитьпротокол, описанный в этом параграфе, некоторым механизмом, который позволял бы отправлять каждое слово повторно (на протяжении интервала отправления слова), до тех пор пока не будет получено подтверждение о его доставке.Интервал отправления должен быть достаточно протяженным, чтобы позволитьосуществлять многократную передачу определенных слов и сделать тем самымвероятность утраты слова как можно меньшей.Со стороны получателя должен срабатывать механизм, который запускаетотправление подтверждающих сообщений при доставке пакета или его получениипри открытом сеансе связи.Ограниченные порядковые номера.
Порядковые номера, используемые в протоколе, можно ограничить, доказав для этого протокола утверждение, аналогичное лемме 3.9 для симметричного протокола раздвижного окна [187, §3.2]. Дляэтого необходимо ввести допущение о том, что скорость поступления слов навход процесса р ограничена таким образом, чтобы очередное слово поступалоспустя не менее U + 2р + R единиц времени после поступления L-ro по порядку предшествующего слова. Чтобы достичь этого, действие Ар нужно снабдитьпредохранителем{(High < L) V (Ut[B + High - L ] < - R - 2p)}.В рамках такого допущения можно показать, что порядковые номера полученных пакетов данных отстоят не более чем на 2L от ожидаемого номера Ехр ,а порядковые номера в подтверждающих сообщениях отстоят не более чем на Lот номера High.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
