скачать рефераты
  RSS    

Меню

Быстрый поиск

скачать рефераты

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

(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) следует splq£ 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 слов.

Страницы: 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, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62


Новости

Быстрый поиск

Группа вКонтакте: новости

Пока нет

Новости в Twitter и Facebook

  скачать рефераты              скачать рефераты

Новости

скачать рефераты

© 2010.