Реферат: Распределенные алгоритмы

Два процесса связи обозначаются как p и q. Предположения, требования и протокол абсолютно симметричны. Вход p состоит из информации, которую он должен послать q, и моделируется неограниченным массивом слов inp. Выход  p состоит из информации, которую он получает от q, и также моделируется неограниченным массивом слов, outp. Предполагается, что p имеет случайный доступ по чтению к  inp  и случайный доступ по записи к outp. Первоначально значение outp[i] не определено и представлено как udef для всех i. Вход и выход процесса  q моделируется массивами inq и outq соответственно. Эти массивы нумеруются натуральными числами, т.е. они начинаются со слова с номером 0. В подразделе 3.1.3 будет показано, что произвольный доступ может быть ограничен доступом к "окну" конечной длины, передвигающемуся вдоль массива. Поэтому протокол называется протоколом «скользящего окна».

Процесс p содержит переменную sp, показывающую наименьшее нумерованное слово, которое p все еще ожидает от q. Таким образом, в любой момент времени, p уже записал слова от outp[0] до outp[sp - 1]. Значение sp  никогда не уменьшается. Аналогично q содержит переменную sq. Теперь могут быть установлены требуемые свойства протокола. Свойство безопасности говорит о том, что каждый процесс передает только корректные данные; свойство живости говорит о том, что все данные когда-либо будут доставлены.

(1) Свойство безопасности. В каждой достижимой конфигурации протокола

outp[0..sp — 1] = inq[0..Sp — 1] и outq[0..sq — 1] = inp [0...sq — 1].

(2) Окончательная доставка. Для каждого целого k ³ 0, конфигурации с sp ³ k и
sq ³ k когда-либо достигаются.

3.1.1 Представление протокола

Протоколы передачи обычно полагаются на использование сообщений подтверждения. Сообщение подтверждения посылается процессом получения, чтобы сообщить отправителю о данных, которые он получил корректно. Если отправитель данных не получает подтверждение, то он предполагает, что данные (или подтверждение) потеряно, и повторно передает те же самые данные. В протоколе этого раздела, однако, не используются явные сообщения подтверждения. В этом протоколе обе станции имеют сообщения, которые нужно послать другой станции; сообщения станции служат также подтверждениями для сообщений другой станции.

Сообщения, которыми обмениваются процессы, называют пакетами, и они имеют форму
< pack, w, i >, где w - слово данных, а i - натуральное число (называемое порядковым номером пакета). Этот пакет, посылаемый процессом p (к q), передает слово = inp[i] для q, но также, как было отмечено, подтверждает получение некоторого количества пакетов от q. Процесс p может быть «впереди» q не более, чем на lp пакетов, если мы потребуем, что пакет данных < pack, w, i >, посланный p, подтверждает получение слов с номерами 0.. i— lp от q. (q посылает аналогичные пакеты.) Константы lp и lq неотрицательны и известны обоим процессам p и q. Использование пакета данных в качестве подтверждения имеет два последствия для протокола:

(1)  Процесс p может послать слово inp[i] (в виде пакета < pack, inp[i], i >) только после того, как запишет все слова от outp[0] до outp[i — lp], т. е. , если i < sp + lp.

(2)  Когда p принимает < pack, w,i>, повторная передача слов с inp[0] до inp[i — lq] уже не нужна.

Объяснение псевдокода. После выбора модели нетрудно разработать код протокола; см. Алгоритм 3.1. Для процесса p введена переменная ap (и aq для q), в которой хранится самое первое слово, для которого p (или q, соответственно) еще не получил подтверждение..

В Алгоритме 3.1 действие Sp - посылка i-го слова процессом p, действие Rp - принятие слова процессом  p, и действие Lp - потеря пакета с местом назначения p. Процесс p может послать любое слово, индекс которого попадает в указанные ранее границы. Когда сообщение принято, в первую очередь делается проверка - было ли идентичное сообщение принято ранее (на случай повторной передачи). Если нет, слово, содержащееся в нем, записывается в выход, и ap и sp корректируются. Также вводятся действия Sq, Rq и Lq , где p и q поменяны ролями.

var sp, ap : integer                  init 0, 0 ;

    inp    : array of word           (* Посылаемые данные *) ;

    outp   : array of word            init udef, udef, ...',

Sp: {ap £ i < Sp+lp}

    begin send < pack,inp[i],i> to q end

Rp: { < pack, w, i > ÎQp }

    begin receive <pack, w, i> ;

          if outp[i] = udef then

             begin outp[i] := w ;

                   ap := max(ap,i-lp+1) ;

                   Sp := minj

             end

           (* else игнорируем, пакет передавался повторно *)

    end

Lp: {<pack,w,i>ÎQp}

begin Qp := Qp\ {<pack,w,i>} end

Алгоритм 3.1 Протокол скользящего окна (для p).

Инвариант протокола. Подсистема связи представляется двумя очередями, Qp для пакетов с адресатом p и Qq, для пакетов с адресатом q. Заметим, что перевычисление sp в Rp никогда не дает значение меньше предыдущего, поэтому sp никогда не уменьшается. Чтобы показать, что этот алгоритм удовлетворяет данным ранее требованиям, сначала покажем, что утверждение P - инвариант. (В этом и других утверждениях i - натуральное число.)

P º      "i < sp : outp[i]¹ udef                                     (0p)

/\ "i < sq, : outq[i] ¹ udef                                             (0q)

/\ < pack, w, i > Î Qp  Þ  w = inq[i] /\ (i < sq + lq)   (lp)

/\ < pack, w, i > Î Qq  Þ  w = inp[i] /\ (i < sp + lp)   (lq)

/\ outp[i]¹ udef  Þ outp[i] = inq[i] /\ (ap > i— lq)     (2p)

/\ outq[i]¹ udef  Þ outq[i] = inp[i] /\ (aq > i— lp)     (2q)

/\ ap £ sq,                                                          (3p)

/\ aq £ sp                                                                       (3q)

Лемма 3.1 P - инвариант Алгоритма 3.1.

Доказательство. В любой начальной конфигурации Qp и Qq - пустые, для всех i, outp[i] и outq[i] равны udef, и ap,ap, sp и sq равны нулю 0; из этого следует, что P=true. Перемещения протокола рассмотрим с точки зрения сохранения значения P. Во-первых, заметим, что значения inp и inq, никогда не меняются.

Sp:  Чтобы показать, что Sp сохраняет (0p), заметим, что Sp не увеличивает sp и не делает ни один из outp[i] равным udef.

Чтобы показать, что Sp сохраняет (0q), заметим, что Sp не увеличивает sq, и не       делает ни один из outq[i] равным udef.

Чтобы показать, что Sp сохраняет (1p), заметим, что Sp не добавляет пакеты в Qp и не уменьшает sp.

Чтобы показать, что Sp сохраняет (lq), заметим Sp добавляет < pack, w, i > в Qp с w = inp[i] и i < sp + lp, и не изменяет значение sp.

Чтобы показать, что Sp сохраняет (2p) и (2q), заметим, что Sp не изменяет значения outp, outq, ap, или aq.

Чтобы показать, что Sp сохраняет (3p) и (3q), заметим, что Sp не меняет значения  ap , ap , sq , или sp.

Rp:  Чтобы показать, что Rp сохраняет (0p), заметим, что Rp не делает ни одно outp[i] равным udef, и если он перевычисляет sp, то оно впоследствии также удовлетворяет (0p).

Чтобы показать, что Rp сохраняет (0q), заметим, что Rp не меняет outq или sq.

Чтобы показать, что Rp сохраняет (lp), заметим, что Rp не добавляет пакеты в Qp и не уменьшает sq.

Чтобы показать, что Rp сохраняет (lq), заметим, что Rp не добавляет пакеты в Qq и не уменьшает sp.

Чтобы показать, что Rp сохраняет (2p), заметим, что Rp изменяет значение outp[i] на w при принятии < pack, w,i>. Т.к. Qp содержала этот пакет до того, как выполнился Rp, из (1p) следует, что w = inp[i]. Присваивание ap:= max (ap, i— lq+1) гарантирует, что ap > i— lq сохраняется после выполнения. Чтобы показать, что Rp сохраняет (2q), заметим, что Rp не меняет значения outq или aq.

Чтобы показать, что Rp сохраняет (3p), заметим, что когда Rp присваивает
ap:= max(ap, i— lq+1) (при принятии  <pack, w,i>), из (lp) следует, что i < sq+lq, следовательно ap £ sq  сохраняется после присваивания. Rp не меняет sq. Чтобы показать, что Rp сохраняет (3q), заметим, что sp может быть увеличен только при выполнении Rp.

Lp   : Чтобы показать, что Lp сохраняет (0p), (0q), (2p), (2q), (3p), и (3q), достаточно заметить, что Lp не меняет состояния процессов. (lp) и (lq) сохраняются потому, что Lp только удаляет пакеты (а не порождает или искажает их).

Процессы  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) следует  outp[0..Sq -1] = inp[0..Sq -1].ð

Чтобы доказать живость протокола, необходимо сделать справедливых предположений и предположение относительно lp и lq. Без этих предположений протокол не удовлетворяет свойству живости, что может быть показано следующим образом. Неотрицательные константы lp и lq еще не определены; если их выбрать равными нулю, начальная конфигурация протокола окажется тупиковой. Поэтому предполагается, что lp + lq > 0.

Конфигурация протокола может быть обозначена g = (cp, cq, Qp, Qq), где cp и cq - состояния  p и q. Пусть g будет конфигурацией, в которой применим Sp (для некоторого i). Пусть

   d = Sp(g) = (cp, cq, Qp, (Qq È {m})),
и отметим, что действие Lq применимо в d. Если  Lq  удаляет m, Lq(d) = g. Отношение Lq(Sp(g)) = g äàåò íà÷àëî íåîãðàíè÷åííûì âû÷èñëåíèÿì, â êîòîðûõ íè sp , ни sq не уменьшаются.

Протокол удовлетворяет требованию «окончательной доставки», если удовлетворяются два следующих справедливых предположения.

Fl. Если посылка пакета возможна в течение бесконечно долгого временно, пакет посылается бесконечно часто.

F2. Если один и тот же пакет посылается бесконечно часто, то он принимается бесконечно часто.

Предположение Fl гарантирует, что пакет посылается снова и снова, если не получено подтверждение; F2 исключает вычисления, подобные описанному выше, когда повторная передача никогда не принимается.

Ни один из двух процессов не может быть намного впереди другого: разница между sp и sq остается ограниченной. Поэтому протокол называется сбалансированным, а также из этого следует, что если требование окончательной доставки удовлетворяется для sp, тогда оно также удовлетворяется для sq, и наоборот. Понятно, что протокол не следует использовать в ситуации, когда один процесс имеет намного больше слов для пересылки, чем другой.

Ëåììà 3.3 Из P следует sp— lq £ ap £ sq £ aq+ lp £ sp + lp.

Äîêàçàòåëüñòâî. Из (0p) и (2p) следует sp— lq£ ap, из (3p) следует  ap£ sp . Из (0q) и (2q)       следует sp £ ap + lp . Из (3q) следует ap + lp £ sp + lp .ð

Òåîðåìà 3.4  Àëãîðèòì 3.1 удовлетворяет требованию окончательной доставки.

Äîêàçàòåëüñòâî. Сначала будет продемонстрировано, что в протоколе невозможны тупики. Из инварианта следует, что один из двух процессов может послать пакет, содержащий слово с номером, меньшим, чем ожидается другим процессом.

Утверждение 3.5 Из P следует, что посылка < pack, in[sq], sq> процессом p или посылка
< pack, inq[sp], sp ) процессом  q возможна.

Äîêàçàòåëüñòâî. Т.к. lp + lq > 0, хотя бы одно из неравенств Ëåììы 3.3 строгое, т.е.,

sq < sp + lp   \/   sp < sq+lq.

Из P также следует ap £ sq (3p) и aq £ sp (3q), а также следует, что

(ap £ sq<sp+lp) \/ (aq £ sp<sq+lq)

это значит, что Sp применим с i = sq или Sq применим с i = sp.       ð

Теперь мы можем показать, что в каждом из вычислений sp и sq увеличиваются бесконечно часто. Согласно Утверждению 3.5 протокол не имеет терминальных конфигураций, следовательно каждое вычисление неограниченно. Пусть C - вычисление, в котором sp и sq увеличиваются ограниченное число раз, и пусть sp and sq - максимальные значения, которые эти переменные принимают в C. Согласно утверждению, посылка <pack, inp[sq], sq> процессом p или посылка <pack, in q[sp], sp > процессом q применима всегда после того, как sp, sq, ap и aq достигли своих окончательных значений. Таким образом, согласно Fl, один из этих пакетов посылается бесконечно часто, и согласно F2, он принимается бесконечно часто. Но, т.к. принятие пакета с порядковым номером sp процессом p приводит к увеличению sp (и наоборот для q), это противоречит допущению, что ни sp, ни sq  не увеличиваются более. Таким образом Òåîðåìà 3.4 доказана.                                                              ð

Мы завершаем этот подраздел кратким обсуждением предположений Fl и F2. F2-ìèíèìàëüíîå требование, которому должен удовлетворять канал, соединяющий p и q, для того, чтобы он мог передавать данные. Очевидно, если некоторое слово inp[i] никогда не проходит через канал, то невозможно достичь окончательной доставки слова. Предположение Fl обычно реализуется в протоколе с помощью условия превышения времени: если ap не увеличилось в течение определенного промежутка времени, inp[ap] передается опять. Как уже было отмечено во введении в эту главу, для этого протокола безопасная доставка может быть доказана без принятия во внимания проблем времени (тайминга).

3.1.3 Обсуждение протокола

Ограничение памяти в процессах. Àëãîðèòì 3.1 не годится для реализации в компьютерной сети, т.к. в каждом процессе хранится бесконечное количество информации (массивы in и out) и т.к. он использует неограниченные порядковые номера. Сейчас будет показано, что достаточно хранить только ограниченное число слов в каждый момент времени. Пусть L = lp + lq.

Ëåììà 3.6 Из P следует, что отправление < pack, w,i> процессом p применимо только для i < ap+L.

Äîêàçàòåëüñòâî. Сторож Sp требует i < sp+lp, значит согласно Ëåììе 3.3 i < ap+L.   ð                                                     

Ëåììà 3.7 Из P следует, что если outp[i]¹ udef, то i < sp + L.

Äîêàçàòåëüñòâî. Из (2p), ap > i— lq, значит i < ap + lq, и i < sp + L (из Ëåììы 3.3). ð 

Ðèñóíîê 3.2 Скользящие окна протокола.

Последствия этих двух лемм отображены на Ðèñóíêе 3.2. Процессу p необходимо хранить только слова inp[ap..sp + lp — 1] потому, что это слова, которые p может послать. Назовем их как  посылаемое окно  p (представлено как S на Ðèñóíêе 3.2). Каждый раз, когда ap увеличивается, p отбрасывает слова, которые больше не попадают в посылаемое окно (они представлены как A на Ðèñóíêе 3.2). Каждый раз, когда sp увеличивается, p считывает следующее слово из посылаемого окна от источника, который производит слова. Согласно Ëåììе 3.6, посылаемое окно процесса p содержит не более L слов.

Подобным же образом можно ограничить память для хранения процессом p массива outp. Т.к. outp[i] не меняется для i < sp, можно предположить, что p выводит эти слова окончательно и более не хранит их (они представлены как W на Ðèñóíêе 3.2). Т.к. outp[i] = udef для всех i ³ sp + L, эти значения outp[i] также не нужно хранить. Подмассив outp[sp..sp +L—1] назовем принимаемое окно p. Принимаемое окно представлено на Ðèñóíêе 3.2 как u для неозначенных слов и R для слов, которые были приняты. Только слова, которые попадают в это окно, хранятся процессом. Леммы 3.6 и 3.7 показывают, что не более 2L слов хранятся процессом в любой момент времени.

Ограничение чисел последовательности. В заключение будет показано, что числа последовательности могут быть ограничены, если используются fifo-каналы. При использовании fifo предположения можно показать, что номер порядковый номер пакета, который получен процессом p  всегда внутри 2L-окрестности sp. Обратите внимание, что fifo предположение используется первый раз.

Ëåììà 3.8 Утверждение P', определяемое как

P' º P

/\ <pack, w, i> is behind <pack, w', i'> in Qp Þ i > i' - L     (4p)

/\ <pack, w, i> is behind <pack, w', i'> in Qq Þ i > i' - L     (4q)

/\ <pack,w,i> ÎQp Þ i³ ap - lp                                               (5p)

/\ <pack,w,i> ÎQq Þ i³ aq - lq                                               (5q)

является инвариантом  Àëãîðèòìа 3.1.

Äîêàçàòåëüñòâî. Т.к. уже было показано, что P - инвариант, мы можем ограничиться доказательством того, что (4p), (4q), (5p) и (5q) выполняются изначально и сохраняются при любом перемещении. Заметим, что в начальном состоянии очереди пусты, следовательно (4p), (4q), (5p) и (5q) очевидно выполняются. Сейчас покажем, что перемещения сохраняют истинность этих утверждений.

Sp: Чтобы показать, что Sp сохраняет (4p) и (5p), заметим, что Sp не добавляет пакетов в Qp и не меняет ap.

Чтобы показать, что Sp сохраняет (5q), заметим, что если Sp добавляет пакет <pack, w, i> в Qq, то i ³ ap, откуда следует, что i³  aq - lq (из Ëåììы 3.3).

Чтобы показать, что Sp сохраняет (4q), заметим, что если < pack, w', i'> в Qq, тогда из (lq)
i' < sp + lp, следовательно, если Sp добавляет пакет < pack, w, i> с i ³ ap, то из Леммы 3.3 следует  i' < ap+L £ i+L.

Rp: Чтобы показать, что Rp сохраняет (4p) and (4q), заметим, что Rp не добавляет пакеты в Qp или Qq.

 Чтобы показать, что Rp сохраняет (5p), заметим, что когда ap увеличивается (при принятии <pack, w', i'>) до   i' - lq +1, тогда для любого из оставшихся пакетов <pack, w, i> в Qp мы имеем i > i' - L (из 4р). Значит неравенство i ³ ap - lp сохраняется после увеличения ap.

Страницы: 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42