Реферат: Распределенные алгоритмы
(1) Рассматриваемые ошибки. Для двух протоколов будут рассматриваться различные классы ошибок передачи. Сообщения не могут пересекаться при физическом соединении, и они не могут быть продублированы; таким образом, в разделе 3.1 рассматривается только потеря сообщений (об искажении сообщений см. ниже). В сети сообщения могут передаваться различными путями, и, следовательно, пересекаться; также, из-за отказов промежуточных станций сообщения могут быть продублированы или потеряны. В Разделе 3.2 будут рассматриваться потеря, дублирование и переупорядочение сообщений.
(2) Управление соединением. Далее, управление соединением не будет рассматриваться для первого протокола, но будет для второго. Предполагается, что физическое соединение функционирует непрерывно в течение очень длительного времени, а не открывается и закрывается неоднократно. Для соединений с удаленными станциями это не так. Такое соединение может быть необходимо временно для обмена некоторыми данными, но обычно слишком дорого поддерживать соединение с каждой удаленной станцией неопределенно долго. Следовательно, для второго протокола будет требоваться способность открывать и закрывать соединение.
При рассмотрении первого протокола показывается, что не только механизмы, основанные на таймерах, могут обеспечить требуемые свойства безопасности протоколов передачи данных. Раздел 3.1 служит первым большим примером доказательства свойств безопасности с помощью инструментальных средств, описанных в Разделе 2.2. Многие полагают [Wat81], что правильное использование таймеров и ограничение на время, в течение которого сообщение может передаваться , необходимы для безопасного управления соединением. Таким образом, для того, чтобы доказать безопасность протоколов, нужно принимать во внимание роль таймеров в управлении соединением. Раздел 3.2 показывается, как модель распределенных систем (Определение 2.6) может быть расширена до процессов, использующих таймеры, и дает пример этого расширения.
Искажение сообщений. Естественно принять во внимание возможность того, что сообщения могут быть искажены в течение передачи. Содержание сообщения, переданного через физическое соединение, может быть повреждено из-за атмосферных шумов, плохо функционирующих модулей памяти, и т.д. Однако можно предположить, что искажение сообщения может быть обнаружено процессом-получателем, например, посредством контроля четности или более общих механизмов контрольной суммы ( [Tan88, Глава 41). Получение искаженного сообщения затем обрабатывается так, как будто не было получено никакого сообщения, и таким образом, искажение сообщения фактически вызывает его потерю. По этой причине искажение не обрабатывается явно; вместо этого всегда рассматривается возможность потери сообщения.
3.1 Сбалансированный протокол скользящего окна
В этом разделе изучается симметричный протокол, который обеспечивает надежный обмен информацией в обоих направлениях. Протокол взят из [Sch91, Глава 2]. Поскольку он используется для обмена информацией между станциями, которые непосредственно соединены через линию, можно предположить, что каналы имеют дисциплину fifo. Это предположение не используется, однако, до Подраздела 3.1.3, где показано, что числа последовательности, используемые протоколом могут быть ограничены. Протокол представлен в Подразделе 3.1.1, а в Подразделе 3.1.2 доказывается его правильность.
Два процесса связи обозначаются как 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
когда-либо достигаются.
Протоколы передачи обычно полагаются на использование сообщений подтверждения. Сообщение подтверждения посылается процессом получения, чтобы сообщить отправителю о данных, которые он получил корректно. Если отправитель данных не получает подтверждение, то он предполагает, что данные (или подтверждение) потеряно, и повторно передает те же самые данные. В протоколе этого раздела, однако, не используются явные сообщения подтверждения. В этом протоколе обе станции имеют сообщения, которые нужно послать другой станции; сообщения станции служат также подтверждениями для сообщений другой станции.
Сообщения, которыми обмениваются процессы, называют пакетами,
и они имеют форму
< 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 - натуральное число.)
Страницы: 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, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105
