Введение в распределённые алгоритмы. Ж. Тель (2009) (1185665), страница 26

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 26)

Процесс р может отправить слово inp[i\ (в пакете (pack, inp[i\, г)) толькопосле того, как будут занесены в память все слова, начиная с outp[0] и заканчиваяoutp[i —1Р], т. е. когда будет выполняться неравенство i < s p + lp.2. Как только р получает пакет (pack, w , i), отпадает необходимость в по­вторной передаче слов, начиная с inp[0] и заканчивая inp[i —lq].Пояснения к псевдокоду. После того как мы сформулировали общие прин­ципы устройства протокола, написать псевдокод протокола уже нетрудно; онпредставлен в алгоритме 3.1.

Переменная ар в процессе р (равно как и пере­менная ач в процессе q) используется для обозначения наименьшего порядко­вого номера того входного слова, для которого процесс р (или соответственнопроцесс q) еще не получил подтверждающего сообщения. В алгоритме 3.1 дей­ствие Sp осуществляет отправление i - го входного слова процесса р, действие R^,осуществляет прием слова процессом р, а действие Lp моделирует потерю паке­та, адресатом которого является процесс р.

Процесс р может отправить любоеГл. 3. Коммуникационные протоколы90слово, порядковый номер i которого находится в тех пределах, которые указаныв действии Sр. Когда процесс получает некоторое сообщение, он вначале про­веряет, не было ли такое же сообщение получено ранее (в этом случае процессимеет дело с повторным получением сообщения). Если это не так, то слово, со­держащееся в сообщении, записывается в выходной массив и при этом значенияпеременных ар и sp изменяются. В процессе q также имеются аналогичные дей­ствия S q, Rp И Ц .Инвариант протокола. Коммуникационная подсистема представлена двумяочередями: очередью пакетов Qp, адресованных процессу р, и очередью пакетовQq, адресованных процессу q. Заметим, что при обновлении значения переменнойsp в действии Rp новое значение никогда не может быть меньшим, чем прежнеезначение, т.

е. значения переменной sp не убывают. Чтобы показать, что алгоритмудовлетворяет тем требованиям, которые были сформулированы выше, покажемсначала, что утверждение Р является инвариантом. И в этом, и в последующихутверждениях i может принимать только натуральные значения.АААААААV/ < s p : outp[i] Ф udefV/ < s q : O U t q [/] Ф udef(pack, да,. i) v Qp -=> w = inq[i] A {i < sq + lq)(pack, да,• i) v Qq => w = inp[i] A (» < sp У I p)outp[i] = inq[i\ A (dp > i - lq)outp[i] ф udef =outq[i] ф udef => OUtq[i] = inp[i\ A (dq > i —Ip)d pФSqdqSpm(0q)(1P)(1*7)(2p)m(3P)(3q)Лемма 3.1.

Утверждение Р является инвариантом алгоритма 3.1.Д о к а з а т е л ь с т в о . В каждой начальной конфигурации очереди Qp и Qqпусты, для всякого i значения outp[i] и outq[i] равны udef, а значения переменныхар, dq, sq и sp равны 0; отсюда следует истинность утверждения Р. Рассмотримпоочередно все переходы протокола и покажем, что при каждом из них утвер­ждение Р сохраняет истинность. Прежде всего отметим, что значения массивовitip и itiq никогда не изменяются.Sp: Чтобы убедиться, что действие Sp сохраняет выполнимость условия (Ор),заметим, что это действие не изменяет значения переменной sp и не записываетв массив outp\i] неопределенного значения udef.Чтобы убедиться, что действие Sp сохраняет выполнимость условия (0q), за­метим, что Sp не увеличивает значения переменной sq и не записывает в массивoutq[i\ неопределенного значения udef.Чтобы убедиться, что действие Sp сохраняет выполнимость условия (1р), за­метим, что Sp не добавляет новых пакетов в очередь Qp и не уменьшает значенияпеременной sq.Чтобы убедиться, что действие Sp сохраняет выполнимость условия (lq), за­метим, что Sp добавляет пакет (pack, да, i) с номером / < sp + 1Р, содержащийслово да = Шр[/], в очередь Qq и при этом значение переменной sp не изменяется.3.1.

Симметричный протокол раздвижного окнаvar sp, аР : integerПрoutp1: array of word: array of word91init 0, 0 ;(* Data to be sent *)init udef, udef, ... ;S„: { aP < i < sP+ lP }begin send (pack, inp[i], i) to q endR • { (pack, да, i) eQP }begin receive (pack, да, 0 ;if outP[i] = udef thenbegin outp[i] = w ;ap := max (ap, i —lq + l) ;sp := min {/I outp[j] = udef}end(* else игнорировать повторное получение пакета *)endLp: { (pack, да, i) eQp }begin Qp := QP\ {(pack, да, i)} endАлгоритм 3.1. Симметричный протокол раздвижного окна (для процесса р).Чтобы убедиться, что действие Sp сохраняет выполнимость условий (2р) и (2q),заметим, что Sp не изменяет значений переменных outp, outq, ар и aq.Чтобы убедиться, что действие Sp сохраняет выполнимость условий (Зр) и (3q),заметим, что Sp не изменяет значений переменных ар, aq, sq и sp.Rp: Чтобы убедиться, что действие Rp сохраняет выполнимость условия (Ор),заметим, что Rp не записывает в массив outp[i] неопределенного значения udef,и если это действие изменяет значение переменной sp, то условие (Ор) сохраняетпри этом выполнимость.Чтобы убедиться, что действие Rp сохраняет выполнимость условия (Oq), за­метим, что Rp не изменяет значений переменных outq и sq.Чтобы убедиться, что действие Rp сохраняет выполнимость условия (1р), за­метим, что Rp не добавляет новых пакетов в очередь Qp и не уменьшает значенияпеременной sq.Чтобы убедиться, что действие Rp сохраняет выполнимость условия (lq), за­метим, что Rp не добавляет новых пакетов в очередь Qq и не уменьшает значенияпеременной sp.Чтобы убедиться, что действие Rp сохраняет выполнимость условия (2р), за­метим, что Rp записывает слово да в элемент outp[i] выходного массива приполучении пакета (pack, да, /).

Так как в очереди Qp уже содержался этот пакет,до того как выполнилось действие Rp, из условия (1р) следует, что да = inq[i\.Присваивание ар := max(ap, i —lq + 1) гарантирует, что неравенство ар > i —lqбудет справедливо и после выполнения этого действия.Чтобы убедиться, что действие Rp сохраняет выполнимость условия (2q), за­метим, что Rp не изменяет значений переменных outq и aq.92Гл. 3.

Коммуникационные протоколыЧтобы убедиться, что действие Rp сохраняет выполнимость условия (Зр), за­метим, что, когда Rp присваивает переменной ар значение т а х(ар, i —lq + 1)(при получении пакета (pack, w, /)), из условия (1р) следует, что неравенство/ < sq + lq останется верным, и, значит, неравенство ар ^ sq будет соблюдатьсяпосле этого присваивания. Действие Rp не изменяет значения переменной sq.Чтобы убедиться, что действие Rp сохраняет выполнимость условия (3q), за­метим, что значение переменной sp может лишь увеличиться после выполнениядействия Rp.Lp: Чтобы убедиться, что действие Lp сохраняет выполнимость условий (Ор),(Oq), (2р), (2q), (Зр) и (3q), достаточно заметить, что Lp не изменяет состоянийобоих процессов.Выполнимость условий (1р) и (lq) сохраняется, поскольку действие Lp лишьудаляет пакеты из очереди, но не вставляет и не искажает никаких пакетов.Аналогично можно проверить, что действия Sq, R9 и L9 также сохраняютистинность утверждения Р.□3.1.2.

Доказательство корректности протоколаТеперь мы покажем, что алгоритм 3.1 обеспечивает надежную (свойство без­опасности) и неизбежную (свойство живости) доставку сообщений. Как будетустановлено в теореме 3.2, свойство безопасности следует из инварианта, а вотс доказательством свойства живости дело обстоит сложнее.Теорема 3.2. Алгоритм 3.1 удовлетворяет требованию безопасной до­ставки сообщений.Д о к а з а т е л ь с т в о . Легко видеть, что из условий (Ор) и (2р) следуетсправедливость равенства outp[Q..sp —1] = inq[0..sp —1], а из условий (Oq) и (2q)следует справедливость равенства outq[0..sq — 1] = inp[0..sq — 1].□Чтобы убедиться в выполнимости свойства живости протокола, необходимоввести в рассмотрение допущения справедливости, а также ввести ограниченияна значения 1Р и lq.

Без этих допущений протокол не будет обладать свойствомживости, и вот почему. В качестве 1Р и lq можно взять любые неотрицательныеконстанты; но если обе константы будут равны 0, то протокол будут заблокировануже в своей конфигурации (т. е. каждая начальная конфигурация будет такжеи заключительной). Поэтому мы будем считать, что соблюдается неравенство1р + lq > 0 .Условимся, что запись у = (ср, cq, Qp, Qq), где ср и cq — состояния процессовр и q, будет обозначать конфигурацию протокола. Рассмотрим произвольнуюконфигурацию у, в которой допустимо действие Sp (при некотором значении /).Пусть8 = Sp(y) = (Ср, Cq, Qp, (Qq U {m})).Заметим, что действие L^ является допустимым в конфигурации 8.

Как толькодействие L^ промоделирует потерю сообщения т, будет выполняться соотноше­ние ЦД8) = у. Равенство L(,(Sp(y)) = у открывает возможность для осуществле­3.1. Симметричный протокол раздвижного окна93ния бесконечного вычисления, в котором значения обеих переменных sp и sq небудут увеличиваться.Протокол будет удовлетворять требованию неизбежной доставки сообщений,если принять во внимание следующие два допущения справедливости.F1.

Если бесконечно часто возникает возможность отправки пакета, то этотпакет будет отправляться бесконечно часто.F2. Если один и тот же пакет отправляется бесконечно часто, то и принима­ется он также бесконечно часто.Допущение F1 гарантирует, что всякий пакет будет отправляться снова и сно­ва, если не будет получено подтверждение его получения; допущение F2 исклю­чает возможность описанных выше вычислений, в которых ни одно из повторныхотправлений одного и того же пакета не приводит к его доставке.Ни один из двух процессов не может уйти вперед от другого слишком далеко:разность величин sp и sq остается ограниченной.

Вот поэтому рассматриваемыйпротокол называется симметричным; если требование неизбежной доставки со­общений выполняется для переменной sp, то оно также выполняется и для sq,и наоборот. Это означает также, что данный протокол нельзя применять в техслучаях, когда одному из процессов нужно отправить существенно больше слов,чем другому.Лемма 3.3.

Из инварианта Р следует неравенство sp —l q ^ ар ^ sq ^^ &q ~\~1р ^ sp -\- 1р.Д о к а з а т е л ь с т в о . Из свойств (Ор) и (2р) вытекает неравенство sp- l q < ар.Свойство (Зр) обеспечивает выполнимость неравенства ар ^ sq. Из свойств (Oq)и (2q) следует неравенство sq ^ aq + lp . И, наконец, из соотношения (3q) следуетнеравенство aq + lp ^ sp + 1Р.□Теорема 3.4. Алгоритм 3.1 удовлетворяет требованию неизбежнойдоставки сообщений.Д о к а з а т е л ь с т в о . Прежде всего убедимся в том, что протокол никогдане может быть заблокирован. Как следует из инварианта, один из двух процессовможет отправлять пакет, содержащий слово с наименьшим порядковым номером,из тех, которые еще не достигли другого процесса.Утверждение 3.5.

Из инварианта Р следует, что допустимыми дей­ствиями являются отправление пакета {pack, inp[sq], sq) процессом р илиотправление пакета {pack, inq[sp], sp) процессом q.Д о к а з а т е л ь с т в о . В рамках допущения lp + lq > 0 по крайней мереодно из неравенств леммы 3.3 является строгим, т. е.sq <с sp -\- lp V sp <с sq “Ь lq.Из инварианта Р также следуют неравенства ар < sq (Зр) и aqэтому справедливо соотношение(ар ^ sq <с sp -\- 1Р) V (aq ^ spsq -Ь lq),sp (3q), и по­94Гл.

3. Коммуникационные протоколыкоторое означает, что либо действие Sp допустимо для i = sq, либо действие Sqдопустимо для i = sp.□Теперь мы можем показать, что в любом вычислении значения переменныхsp и sq возрастают бесконечно часто. Согласно утверждению 3.5 протокол недостигает заключительных конфигураций, и поэтому каждое вычисление продол­жается бесконечно долго.

Характеристики

Список файлов книги