Введение в распределённые алгоритмы. Ж. Тель (2009) (1185665), страница 32
Текст из файла (страница 32)
Следовательно, при передаче увеличение порядковых номеровможно проводить по модулю 2L.Облик действий и инвариантов. Теоретико-доказательный подход сводитанализ коммуникационного протокола к задаче проверки и преобразования формул (иногда весьма громоздких). Манипуляции с формулами — это очень «на-112Гл. 3. Коммуникационные протоколыдежный» прием, потому что на каждом шаге можно провести очень тщательнуюпроверку и вероятность ошибки чрезвычайно мала. И все же есть определенныйриск того, что при этом может быть потеряно общее понимание протокола и егосвязь с рассматриваемыми формулами. Вопрос об устройстве протокола можно осмыслить как с прагматической, так и с формальной точки зрения.
Флетчер и Ватсон в работе [85] настаивают на том, что управляющая информациядолжна быть «защищена», имея в виду, что ее смысл не должен изменяться приутрате или дублировании пакетов; такова прагматическая точка зрения. При использовании теоретико-доказательного подхода к решению задачи верификации«смысл» управляющей информации проявляется в выборе тех или иных утверждений в качестве инвариантов. Формальный взгляд на устройство протоколаопределяется выбором этих инвариантов и устройством переходов, сохраняющихэти инварианты. На самом деле, как будет показано далее, замечание Флетчераи Ватсона можно переформулировать в терминах описания структуры формул,которые разрешается или не разрешается использовать в качестве инвариантовпротокола, стойкого по отношению к потерям и дублированию пакетов.Все соотношения (дизъюнкты), входящие в состав формулы Р 2 и касающиесяпакетов, имеют следующий общий вид:Vm е М : А(т),и, как нетрудно убедиться, выполнимость соотношений такого вида сохраняетсяпри дублировании или потере пакетов.
В последующих главах мы будем рассматривать инварианты более общего вида, напримерЕ/("») = кт£МИЛИпредусловие =$■ З т Е М : А(т).Предложения такого вида могут утратить истинность в случае потери или дублирования пакетов, и поэтому их нельзя использовать при доказательстве корректности алгоритмов, от которых требуется устойчивость по отношению к подобнымсбоям.Аналогичное замечание касается устройства инвариантов, относящихся к действию Time. Как уже говорилось, это действие сохраняет выполнимость всехпредложений видаX t ^ Y t + С,где Xt и Yt — таймеры, а С — константа.Неточные таймеры. Действие Time моделирует идеальные таймеры, значения которых уменьшается в точности на 8 по истечении 8 единиц времени, нона практике таймеры подвержены неточностям, которые называются расхождениями.
Обычно предполагается, что это расхождение является г-ограниченнымдля некоторой известной константы е. Это означает, что за период времени длины8 показания таймера уменьшаются на величину 8', которая удовлетворяет неравенству 8/(1 + е) ^ 8' ^ 8 х (1 +е). (Обычно е является величиной порядка 10-53.2. Протокол с таймерами113Time-s: { В > 0 }begin (* Значения всех таймеров процесса р уменьшаются на В' *)*':=■■■ ;(* ( п Ь ) ^ 8' ^ 8 x ( i + S) *)forall i do Ut[i\ := Ut[i\ — 8' ;St := S t - 8 ' ;(* Значения всех таймеров процесса q уменьшаются на 8" *)*":=■■■ ;(* (ТТ7) ^ 8" ^ 8 х (1+ £) *)Rt := Rt - 8" ;if Rt < 0 then delete (Rt, Exp) ;(* Поля p вычисляются точно *)forall (.., p) € Mp, Mq dobegin p := p — 8 ;if p < 0 then remove packetendendАлгоритм 3.8.
Модифицированное действие Timeили 10_6.) Такое поведение таймеров моделируется действием Time-e, котороеописано алгоритмом 3.8.Как уже отмечалось ранее, действие Time сохраняет выполнимость предложений вида X t > Y t + C , потому что значения таймеров в обеих частях неравенствауменьшаются на одну и ту же величину, и неравенство Xt > Yt + С влечет соотношение ( X t —8) > (Yt —8) + С.
Аналогичное замечание относится и к действиюTime-e. Для действительных чисел Xt, Yt, 8, 8', Ь", г и с , удовлетворяющих неравенствам 8 > 0 и г > 1, соотношение[Xt > г2 Yt + с]A^ S '< 8 x r )Л^ 8" ^ 8 х г)влечет неравенство(Xt - 8') > г2 (Yt - 8") + с.Следовательно, действие Time-e сохраняет выполнимость предложений видаX t ^ ( 1 + г)2 Yt + с.Наш протокол теперь можно так модифицировать, чтобы он мог работатьс расходящимися таймерами; инварианты при этом преобразуются соответствующим образом. Для того чтобы другие действия также сохраняли выполнимостьмодифицированных инвариантов, константы R и S, используемые в протоколе,должны удовлетворять соотношениямR ^ (1 + е)((1 + б){/ + (1 + s)2p) и S ^ (1 + е)(2р + (1 + t)R).В остальном, за исключением указанных констант, протокол остается без изменений.
Его инвариант представлен на рис. 3.9.Гл. 3. Коммуникационные протоколы114Р'2 =St € Sсг =>■ 0 < Rt ^ RV i < В + High: Ut[i] < UV ( . . . , р) € М р , Mq : О < р < ц(data, s, i, w, р) € Mq = > cs A St Js (1 + e)(p + (i + (1 + z)R)cr =>■ cs A St > (1 + e)((l + z)Rt + p)(ack, i, p) 6 Mp =>■ cs Л S t > (1 + s) x p(data, s, г, ay, p) e Mq =>■ (ay = inp[B + i\ A i < High)-ics =>■ V i < B: Ok(i )cs =>■ V i < В + Low: Ok(i)(data, tr u e , I, w, p) € АД =>■ V г < В + / : 0/г(г)cs =>■АЛЛЛAЛЛAЛAЛ cr =>■ V г < В + Ехр: О Щ )Л (аск, /, р) € М р =>■ V г < В + / : Ok(i)A (data, s, г, w, р) € АД ==>■ t/t[B + г] > (1 + е)(р - р)Л h < г'г < В + High =>■ t/t[ti] < бДг'г]Л сг =>■ Bt > (1 + е)((1 + е )Ut[pr] + (1 + е)2р)Л рг < В + High A Ut[pr] > - ( 1 + е)[! =>■ сгАсг =>■Рис.В + Exp = рг+ 1Л(10(20(30(40(50(60(70(80(90(100(ПО(120(130(140(150(160(170(1803.9.
Инвариант протокола с расходящимися таймерами.Теорема 3.16. Ф о р м у л а Р'2 я в л я е т с я и н в а р и а н т о м п р о т о к о л а с т а й м ерам и, им ею щ им и z -о гр а н и ч ен н о е расхож дение. Э т о т п р о т о к о л уд о влет воряет т ребованиям от сут ст вия пот ерь и упорядочения.3.3.
Упражнения к главе 33.3.1Упражнение 3.1. Покажите, что симметричный протокол раздвижного окнане удовлетворяет требованию непременной доставки сообщения, если из двухдопущений справедливости F1 и F2 выполняется только допущение F2.Упражнение 3.2.
Докажите, что если в симметричном протоколе раздвижного окна L = 1 и начальные значения переменных а р и a q равны —lq и —1Р, торавенства а р + l q = s p и a q + lp = s q всегда выполняются.3.3.2Упражнение 3.3. В протоколе с таймерами отправитель может занести в отчет слово как возможно утраченное, в то время как это слово было благополучнодоставлено получателю.1. Опишите выполнение этого протокола, в ходе которого происходит подобный эффект.2. Можно ли разработать такой протокол, в котором отправитель за ограниченное время составляет отчет об ошибке в т о м и т о л ь к о т о м с л у ч а е , когдаслово не доставляется получателю?3.3. Упражнения к главе 3115Упражнение 3.4. Предположим, что в связи с выходом из строя часовогомеханизма получатель не может закрыть сеанс связи вовремя. Опишите вычисление протокола с таймерами, в ходе которого слово будет утрачено, но отправительне сможет отметить это в отчете.Упражнение 3.5.
Опишите такое вычисление протокола с таймерами, в ходекоторого получатель открывает сеанс связи после получения пакета с порядковым номером, большим нуля.Упражнение 3.6. Действие Time-e не моделирует расхождение оставшегосявремени жизни пакета. Почему?Упражнение 3.7. Докажите теорему 3.16.Упражнение 3.8. Проектировщик сети хотел бы воспользоваться протоколом с таймерами, но при этом желает, чтобы о возможно утраченных словахзапись в отчете осуществлялась ранее. Для этого он модифицирует действие Ерследующим образом:Ер: (* Сформировать отчет об ошибке для возможно утраченного слова *){ Ut[B + Low] < 0 }begin error[B + Low ] := true ; Low := Low + 1 endБудет ли модифицированный таким образом протокол удовлетворять требованиям отсутствия потерь и упорядочения или для этого необходимо внести такжедругие изменения? Каковы, по Вашему мнению, преимущества и недостатки указанной модификации?ГЛАВА4АЛГОРИТМЫ МАРШРУТИЗАЦИИВ общем случае процесс (узел в компьютерной сети) непосредственно не соединен каналами связи с каждым другим процессом.
Из каждого узла пакетыинформации могут непосредственно передаваться только некоторому подмножеству других узлов, которые называются соседями этого узла. Маршрутизация —это термин, который используется для описания процедуры принятия решенияо том, какому соседу (иногда не единственному) следует переслать пакет, чтобыон в конце концов был доставлен по назначению. Цель, которая ставится припроектировании алгоритма маршрутизации, состоит в том, чтобы снабдить каждый узел процедурой, которая сможет выполнять эту функцию и гарантироватьдоставку каждого пакета.Ясно, что в каждом узле должна храниться некоторая информация о топологии сети, и локальная процедура должна принимать решение на основе этойинформации; эту информацию мы будем называть таблицей маршрутизации.Как только введены эти таблицы, задачу маршрутизации можно разбить на двеалгоритмические составляющие; определение структуры таблицы, конечно, является составной частью разработки алгоритма.1.
Вычисление таблиц. Таблицы маршрутизации должны быть вычисленыпри инициализации сети и должны быть обновлены при изменении топологиисети.2. Продвижение пакета. Когда пакет пересылается по сети, для его продвижения используются таблицы маршрутизации.Критерии оценки качества методов маршрутизации учитывают следующие пока затели.1. Корректность. Алгоритм должен доставлять каждый пакет, поступивший в сеть, в точности по назначению.2. Эффективность. Алгоритм должен отправлять пакеты по «наилучшим»путям; например, ожидается, что выбранные пути приводят к небольшой задержке и обеспечивают высокую пропускную способность всей сети.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
