Введение в распределённые алгоритмы. Ж. Тель (2009) (не распознанно) (1185664), страница 25
Текст из файла (страница 25)
Тем не менее можно предполагать, что процесс-получатель способен обнаруживать искажения сообщений, например, при помощи счетчиков четности или более общих методов обнаружения ошибок (об этом рассказано в ра-88Гл. 3. Коммуникационные протоколыботе [182, гл. 3]). В таком случае к получению искаженного сообщения можноотноситься так, как будто никакого сообщения не было получено, и это означает,что искажение сообщения может быть приравнено к потере сообщения.
Поэтомумы не уделяем особого внимания искажениям сообщений, но всегда учитываемвероятность того, что сообщение может быть потеряно.3.1. Симметричный протокол раздвижного окнаВ этом параграфе изучается симметричный протокол, надежный двусторонний обмен информацией. Этот протокол позаимствован из работы [173, гл. 2] .Поскольку он служит для обмена информацией между станциями, соединеннымипрямой линией связи, можно предполагать, что в каналах связи поддерживаетсяочередность сообщений.
Однако это допущение не будет приниматься в расчетвплоть до § 3.1.3, в котором будет показано, что используемая в протоколе нумерация элементов последовательности может быть ограничена. Описание протокола приведено в § 3.1.1, а его корректность доказана в § 3.1.2.Два взаимодействующих процесса будут обозначаться буквами p и q. Описание протокола, а также все допущения и требования относятся к процессу pв той же мере, в какой они относятся к процессу q. Входными данными процессаp является та информация, которую он должен отправить процессу q, эта информация моделируется бесконечным массивом слов in p .
Выходными даннымипроцесса p является та информация, которую он получает от процесса q, и онатакже моделируется бесконечным вектором слов out p . Считается, что p имеетпроизвольный доступ для чтения элементов массива in p и произвольный доступдля записи в массив outp . Первоначально элементы outp [i] для каждого i имеютнеопределенное значение udef. Вход и выход процесса q соответственно моделируются массивами inq и outq . Для индексации элементов массивов используютсянатуральные числа, и нумерация элементов начинается с нуля. Как будет показано в § 3.1.3, вместо произвольного доступа к массивам можно ограничитьсядоступом к «окну» конечного размера, которое перемещается по массиву.
Вотпоэтому этот протокол часто называют «протоколом раздвижного окна».В процессе p имеется переменная sp , служащая для обозначения наименьшего номера того слова, которое процесс p все еще ожидает получить от процесса q.Таким образом, в каждый момент времени участок массива, начинающийся элементом outp [0] и оканчивающийся элементом outp [sp − 1] , уже заполнен процессом p. Значение переменной sp не убывает. Совершенно аналогичная переменнаяsq имеется в процессе q. Теперь мы можем сформулировать те требования, которые предъявляются к протоколу.
Свойство безопасности предписывает каждомупроцессу формировать на выходе только правильные данные, а свойство живостипредусматривает, что все данные рано или поздно достигнут назначения.1. Безопасная доставка данных. В каждой достижимой конфигурации протокола выполняются соотношенияoutp [0..sp − 1] = inq [0..sp − 1]и outq [0..sq − 1] = inp [0..sq − 1] .3.1. Симметричный протокол раздвижного окна892. Неизбежная доставка сообщений. Для каждого целого числа k > 0в ходе выполнения протокола будет достигнута конфигурация, в которой s p > kи sq > k.3.1.1.
Описание протоколаОбычно в протоколах передачи данных значительную роль играют подтверждающие сообщения. Подтверждающее сообщение посылается процессом-получателемчтобы оповестить процесс-отправитель о том, что данные были успешно доставлены по назначению. Если отправитель данных не получает подтверждение, онпередает те же самые данные повторно исходя из предположения о том, что этиданные (или подтверждение об их получении) были потеряны. Однако в протоколе, который описан в этом параграфе, подтверждающие сообщения в явном видене фигурируют. В рассматриваемом протоколе на обеих станциях есть сообщения, которые они должны отправить друг другу; для каждой станции ее входныеданные используются для подтверждения получения сообщений от другой станции.Сообщения, которыми обмениваются процессы, называются пакетами; пакет представляет собой набор вида hpack, w, ii, где w — информационное слово,а i — натуральное число, которое называется порядковым номером пакета.
Этотпакет, будучи отправленным процессом p (по назначению q), не только передаетслово w = inp [i] процессу q, но также, как было отмечено выше, служит подтверждением тому, что ряд пакетов, отправленных процессом q, был успешнополучен. Процесс p может «опережать» процесс q на некоторое заданное числопакетов lp , если мы постановим, что отправление пакета hpack, w, ii процессом pподтверждает получение слов с номерами 0, . .
. , i − l p от процесса q. (То же самоезначение придается пакетам, которые отправляются процессом q.) Константы l pи lq — это неотрицательные целые числа, известные процессам p и q. Использование пакетов данных в качестве подверждающих сообщений имеет двоякиепоследствия для переходов рассматриваемого протокола.1. Процесс p может отправить слово inp [i] (в пакете hpack, inp [i] , ii) толькопосле того, как будут занесены в память все слова, начиная с out p [0] и заканчиваяoutp [i − lp ] , т. е.
когда будет выполняться неравенство i < s p + lp .2. Как только p получает пакет hpack, w, ii, отпадает необходимость в повторной передаче слов, начиная с inp [0] и заканчивая inp [i − lq ] .Пояснения к псевдокоду. После того как мы сформулировали общие принципы устройства протокола, написать псевдокод протокола уже нетрудно; онпредставлен в алгоритме 3.1. Переменная ap в процессе p (равно как и переменная aq в процессе q) используется для обозначения наименьшего порядкового номера того входного слова, для которого процесс p (или соответственнопроцесс q) еще не получил подтверждающего сообщения.
В алгоритме 3.1 действие Sp осуществляет отправление i-го входного слова процесса p, действие Rpосуществляет прием слова процессом p, а действие L p моделирует потерю пакета, адресатом которого является процесс p. Процесс p может отправить любое90Гл. 3. Коммуникационные протоколы3.1. Симметричный протокол раздвижного окнаслово, порядковый номер i которого находится в тех пределах, которые указаныв действии Sp . Когда процесс получает некоторое сообщение, он вначале проверяет, не было ли такое же сообщение получено ранее (в этом случае процессимеет дело с повторным получением сообщения).
Если это не так, то слово, содержащееся в сообщении, записывается в выходной массив и при этом значенияпеременных ap и sp изменяются. В процессе q также имеются аналогичные действия Sq , Rq и Lq .Инвариант протокола. Коммуникационная подсистема представлена двумяочередями: очередью пакетов Qp , адресованных процессу p, и очередью пакетовQq , адресованных процессу q. Заметим, что при обновлении значения переменнойsp в действии Rp новое значение никогда не может быть меньшим, чем прежнеезначение, т.
е. значения переменной sp не убывают. Чтобы показать, что алгоритмудовлетворяет тем требованиям, которые были сформулированы выше, покажемсначала, что утверждение P является инвариантом. И в этом, и в последующихутверждениях i может принимать только натуральные значения.P≡∧∧∧∧∧∧∧∀i < sp : outp [i] 6= udef∀i < sq : outq [i] 6= udefhpack, w, ii ∈ Qp =⇒ w = inq [i] ∧ (i < sq + lq)hpack, w, ii ∈ Qq =⇒ w = inp [i] ∧ (i < sp + lp)outp [i] 6= udef =⇒ outp [i] = inq [i] ∧ (ap > i − lq)outq [i] 6= udef =⇒ outq [i] = inp [i] ∧ (aq > i − lp)ap 6 s qaq 6 s p(0p)(0q)(1p)(1q)(2p)(2q)(3p)(3q)Лемма 3.1.
Утверждение P является инвариантом алгоритма 3.1.Д о к а з а т е л ь с т в о. В каждой начальной конфигурации очереди Q p и Qqпусты, для всякого i значения outp [i] и outq [i] равны udef, а значения переменныхap , aq , sq и sp равны 0; отсюда следует истинность утверждения P. Рассмотримпоочередно все переходы протокола и покажем, что при каждом из них утверждение P сохраняет истинность. Прежде всего отметим, что значения массивовinp и inq никогда не изменяются.Sp : Чтобы убедиться, что действие Sp сохраняет выполнимость условия (0p),заметим, что это действие не изменяет значения переменной s p и не записываетв массив outp [i] неопределенного значения udef.Чтобы убедиться, что действие Sp сохраняет выполнимость условия (0q), заметим, что Sp не увеличивает значения переменной sq и не записывает в массивoutq [i] неопределенного значения udef.Чтобы убедиться, что действие Sp сохраняет выполнимость условия (1p), заметим, что Sp не добавляет новых пакетов в очередь Qp и не уменьшает значенияпеременной sq .Чтобы убедиться, что действие Sp сохраняет выполнимость условия (1q), заметим, что Sp добавляет пакет hpack, w, ii с номером i < sp + lp , содержащийслово w = inp [i] , в очередь Qq и при этом значение переменной sp не изменяется.var sp , ap : integerinp: array of wordoutp: array of word91init 0, 0 ;(* Data to be sent *) ;init udef, udef, .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
