Введение в распределённые алгоритмы. Ж. Тель (2009) (не распознанно) (1185664), страница 26
Текст из файла (страница 26)
. . ;Sp : { a p 6 i < s p + l p }begin send hpack, inp [i] , ii to q endRp : { hpack, w, ii ∈Qp }begin receive hpack, w, ii ;if outp [i] = udef thenbegin outp [i] := w ;ap := max (ap , i − lq + 1) ;sp := min {j| outp [j] = udef}end(* else игнорировать повторное получение пакета *)endLp : { hpack, w, ii ∈Qp }begin Qp := Qp \ {hpack, w, ii} endАлгоритм 3.1. Симметричный протокол раздвижного окна (для процесса p).Чтобы убедиться, что действие Sp сохраняет выполнимость условий (2p) и (2q),заметим, что Sp не изменяет значений переменных outp , outq , ap и aq .Чтобы убедиться, что действие Sp сохраняет выполнимость условий (3p) и (3q),заметим, что Sp не изменяет значений переменных ap , aq , sq и sp .Rp : Чтобы убедиться, что действие Rp сохраняет выполнимость условия (0p),заметим, что Rp не записывает в массив outp [i] неопределенного значения udef,и если это действие изменяет значение переменной s p , то условие (0p) сохраняетпри этом выполнимость.Чтобы убедиться, что действие Rp сохраняет выполнимость условия (0q), заметим, что Rp не изменяет значений переменных outq и sq .Чтобы убедиться, что действие Rp сохраняет выполнимость условия (1p), заметим, что Rp не добавляет новых пакетов в очередь Qp и не уменьшает значенияпеременной sq .Чтобы убедиться, что действие Rp сохраняет выполнимость условия (1q), заметим, что Rp не добавляет новых пакетов в очередь Qq и не уменьшает значенияпеременной sp .Чтобы убедиться, что действие Rp сохраняет выполнимость условия (2p), заметим, что Rp записывает слово w в элемент outp [i] выходного массива приполучении пакета hpack, w, ii.
Так как в очереди Q p уже содержался этот пакет,до того как выполнилось действие Rp , из условия (1p) следует, что w = inq [i] .Присваивание ap := max (ap , i − lq + 1) гарантирует, что неравенство ap > i − lqбудет справедливо и после выполнения этого действия.Чтобы убедиться, что действие Rp сохраняет выполнимость условия (2q), заметим, что Rp не изменяет значений переменных outq и aq .92Гл. 3. Коммуникационные протоколы3.1. Симметричный протокол раздвижного окнаЧтобы убедиться, что действие Rp сохраняет выполнимость условия (3p), заметим, что, когда Rp присваивает переменной ap значение max (ap , i − lq + 1)(при получении пакета hpack, w, ii), из условия (1p) следует, что неравенствоi < sq + lq останется верным, и, значит, неравенство ap 6 sq будет соблюдатьсяпосле этого присваивания.
Действие Rp не изменяет значения переменной sq .Чтобы убедиться, что действие Rp сохраняет выполнимость условия (3q), заметим, что значение переменной sp может лишь увеличиться после выполнениядействия Rp .Lp : Чтобы убедиться, что действие Lp сохраняет выполнимость условий (0p),(0q), (2p), (2q), (3p) и (3q), достаточно заметить, что L p не изменяет состоянийобоих процессов.Выполнимость условий (1p) и (1q) сохраняется, поскольку действие L p лишьудаляет пакеты из очереди, но не вставляет и не искажает никаких пакетов.Аналогично можно проверить, что действия Sq , Rq и Lq также сохраняютистинность утверждения P.3.1.2. Доказательство корректности протоколаТеперь мы покажем, что алгоритм 3.1 обеспечивает надежную (свойство безопасности) и неизбежную (свойство живости) доставку сообщений.
Как будетустановлено в теореме 3.2, свойство безопасности следует из инварианта, а вотс доказательством свойства живости дело обстоит сложнее.Теорема 3.2. Алгоритм 3.1 удовлетворяет требованию безопасной доставки сообщений.Д о к а з а т е л ь с т в о. Легко видеть, что из условий (0p) и (2p) следуетсправедливость равенства outp [0..sp − 1] = inq [0..sp − 1] , а из условий (0q) и (2q)следует справедливость равенства outq [0..sq − 1] = inp [0..sq − 1] .Чтобы убедиться в выполнимости свойства живости протокола, необходимоввести в рассмотрение допущения справедливости, а также ввести ограниченияна значения lp и lq .
Без этих допущений протокол не будет обладать свойствомживости, и вот почему. В качестве lp и lq можно взять любые неотрицательныеконстанты; но если обе константы будут равны 0, то протокол будут заблокировануже в своей конфигурации (т. е. каждая начальная конфигурация будет такжеи заключительной). Поэтому мы будем считать, что соблюдается неравенствоlp + lq > 0.Условимся, что запись = (cp , cq , Qp , Qq), где cp и cq — состояния процессовp и q, будет обозначать конфигурацию протокола. Рассмотрим произвольнуюконфигурацию , в которой допустимо действие S p (при некотором значении i).Пусть= Sp ( ) = (cp , cq , Qp , (Qq ∪ {m})).Заметим, что действие Lq является допустимым в конфигурации .
Как толькодействие Lq промоделирует потерю сообщения m, будет выполняться соотношение Lq ( ) = . Равенство Lq (Sp ( )) = открывает возможность для осуществле-93ния бесконечного вычисления, в котором значения обеих переменных s p и sq небудут увеличиваться.Протокол будет удовлетворять требованию неизбежной доставки сообщений,если принять во внимание следующие два допущения справедливости.F1. Если бесконечно часто возникает возможность отправки пакета, то этотпакет будет отправляться бесконечно часто.F2. Если один и тот же пакет отправляется бесконечно часто, то и принимается он также бесконечно часто.Допущение F1 гарантирует, что всякий пакет будет отправляться снова и снова, если не будет получено подтверждение его получения; допущение F2 исключает возможность описанных выше вычислений, в которых ни одно из повторныхотправлений одного и того же пакета не приводит к его доставке.Ни один из двух процессов не может уйти вперед от другого слишком далеко:разность величин sp и sq остается ограниченной.
Вот поэтому рассматриваемыйпротокол называется симметричным; если требование неизбежной доставки сообщений выполняется для переменной sp , то оно также выполняется и для sq ,и наоборот. Это означает также, что данный протокол нельзя применять в техслучаях, когда одному из процессов нужно отправить существенно больше слов,чем другому.Лемма 3.3. Из инварианта P следует неравенство sp − lq 6 ap 6 sq 66 aq + lp 6 s p + lp .Д о к а з а т е л ь с т в о. Из свойств (0p) и (2p) вытекает неравенство s p −lq 6 ap .Свойство (3p) обеспечивает выполнимость неравенства a p 6 sq . Из свойств (0q)и (2q) следует неравенство sq 6 aq + lp .
И, наконец, из соотношения (3q) следуетнеравенство aq + lp 6 sp + lp .Теорема 3.4. Алгоритм 3.1 удовлетворяет требованию неизбежнойдоставки сообщений.Д о к а з а т е л ь с т в о. Прежде всего убедимся в том, что протокол никогдане может быть заблокирован. Как следует из инварианта, один из двух процессовможет отправлять пакет, содержащий слово с наименьшим порядковым номером,из тех, которые еще не достигли другого процесса.Утверждение 3.5. Из инварианта P следует, что допустимыми действиями являются отправление пакета hpack, inp [sq ] , sq i процессом p илиотправление пакета hpack, inq [sp ] , sp i процессом q.Д о к а з а т е л ь с т в о. В рамках допущения lp + lq > 0 по крайней мереодно из неравенств леммы 3.3 является строгим, т.
е.sq < s p + l p ∨ s p < s q + l q .Из инварианта P также следуют неравенства ap 6 sq (3p) и aq 6 sp (3q), и поэтому справедливо соотношение(ap 6 sq < sp + lp) ∨ (aq 6 sp < sq + lq),94Гл. 3. Коммуникационные протоколы3.1. Симметричный протокол раздвижного окна95которое означает, что либо действие Sp допустимо для i = sq , либо действие Sqдопустимо для i = sp .На самом деле, как будет показано далее, в каждый момент времени процессамдостаточно хранить лишь ограниченное количество слов. Пусть L = l p + lq .Теперь мы можем показать, что в любом вычислении значения переменныхsp и sq возрастают бесконечно часто.
Согласно утверждению 3.5 протокол недостигает заключительных конфигураций, и поэтому каждое вычисление продолжается бесконечно долго. Допустим, что существует вычисление C, в которомзначения переменных sp и sq увеличиваются лишь конечное число раз, и пустьp и q — наибольшие значения, которые могут принимать эти переменные походу вычисления C. Согласно доказанному утверждению либо отправление пакета hpack, inp [ q ] , q i процессом p, либо отправление пакета hpack, in q [ p ] , p iпроцессом q допустимо бесконечно долго, после того как переменные s p , sq , apи aq примут свои окончательные значения. Таким образом, согласно допущениюF1 один из этих пакетов отправляется бесконечно часто, а согласно допущениюF2 он должен приниматься также бесконечно часто.
Но поскольку получениепроцессом p пакета с порядковым номером sp приводит к тому, что значение spувеличивается (и то же самое справедливо для процесса q), возникает противоречие с предположением о том, что значения переменных s p и sq больше не будутувеличиваться. Этим завершается доказательство теоремы 3.4 1) .Лемма 3.6.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
