Распределенные алгоритмы (стр. 20 из 85)

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

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

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

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

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

Ëåììà 3.3 Из P следует s_p— l_q£ a_p£ s_q£ a_q+ l_p £ s_p + l_p.

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

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

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

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

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

sq < sp + lp &bsol;/ sp < sq+lq.

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

(ap £ sq<sp+lp) &bsol;/ (aq £ sp<sq+lq)

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

Теперь мы можем показать, что в каждом из вычислений sp и sq увеличиваются бесконечно часто. Согласно Утверждению 3.5 протокол не имеет терминальных конфигураций, следовательно каждое вычисление неограниченно. Пусть C - вычисление, в котором sp и sq увеличиваются ограниченное число раз, и пусть s_pand s_q - максимальные значения, которые эти переменные принимают в C. Согласно утверждению, посылка <pack, in_p[s_q], s_q> процессом p или посылка <pack, in _q[s_p], s_p > процессом q применима всегда после того, как s_p, s_q, a_p и a_q достигли своих окончательных значений. Таким образом, согласно Fl, один из этих пакетов посылается бесконечно часто, и согласно F2, он принимается бесконечно часто. Но, т.к. принятие пакета с порядковым номером sp процессом p приводит к увеличению sp (и наоборот для q), это противоречит допущению, что ни s_p, ни s_q не увеличиваются более. Таким образом Òåîðåìà 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-окрестности s_p. Обратите внимание, что fifo предположение используется первый раз.

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

P' º P

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

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

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

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

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

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

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

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

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

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

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